``Mathematics is a game played according to certain simple rules with
meaningless marks on paper.''
This quote, attributed to David Hilbert, sums up what one may call the
`syntactic', `operational', `proof theoretic', Post-system approach to
reasoning, programming, and reasoning about programming. Computation
is re-writing of formulas -- programs or program configurations --
until a formula of a particular shape emerges, taken to be the
result. Type checking is putting together a typing judgement like a zigzaw
puzzle. Optimization is also a mechanical re-writing. The popular
textbook `Types and programming languages' is all about reductions and
derivations, syntactic manipulations of formulas -- expressions and
propositions. Denotational semantics is barely a passing mention.

There is an alternative: `semantic', `denotational', `model theoretic' -- aiming to give meaning to the `marks on paper' by relating them to real world, or a model theoreof, to something with which we have experience and intuition. Whereas operational reasoning is confined to rewriting rules -- that's all there is, -- denotational semantics lets us use whatever knowledge and intuition we have about our model. Denotational semantics excels at proving equational laws, used for reasoning and optimization. Denotational semantics also leads to optimization directly: normalization-by-evaluation, or optimization by calculation rather than rewriting.

This web page collects examples of applying the semantic, denotational approach to a variety of problems -- making a case for semantics.

- What are denotations, exactly?
- Tagless-final style

Doing a tagless-final embedding is literally writing the denotational semantics for a DSL -- in a host programming language rather than on paper - Sound and Efficient
Language-Integrated Query -- Maintaining the ORDER

Easy and practical denotational semantics for query optimization - lambda to SKI:
the first compositional translation

Converting a lambda-term to a combinator formula by calculation - Context-Free Grammars: the epitome of many-sorted algebras

Denotational semantics as the initial algebra semantics - Tagless-final optimizations, algebraically and semantically.
- Effects Without Monads:
Non-determinism -- Back to the Meta Language

Abstract interpretation and code generation as (non-standard) denotational semantics - Evaluators, Normalizers, Reducers: from denotational to operational semantics
- Polynomial Event Semantics:
Non-Montagovian Proper Treatment of Quantifiers

Constructing a model for sentences with quantifiers - Stream Fusion, to Completeness

Stream fusion as normalization-by-evalutaion

- Denotational semantics is often described (see, e.g., Wikipedia) as giving
interpretations to expressions (syntactic objects) through
*mathematical objects*. What are those things, precisely? Can OCaml code be a `mathematical object'? It is worth to take a moment to reflect on what exactly denotational semantics is.One of the first definitions of denotational semantics (along with many other firsts) is given by Landin (Landin 1966, Sec 8):

``The commonplace expressions of arithmetic and algebra have a certain simplicity that most communications to computers lack. In particular, (a) each expression has a nesting subexpression structure, (b) each subexpression denotes something (usually a number, truth value or numerical function), (c) the thing an expression denotes, i.e., its `value', depends only on the values of its subexpressions, not on other properties of them.''In the reference text (Mosses 1990, Sec 3.1), Mosses essentially repeats Landin's definition, adding: ``It should be noted that the semantic analyst is free to

*choose*the denotations of phrases -- subject to compositionality''. He notes that letting phrases denote themselves is technically compositional and hence may be accepted as a denotational semantics -- which however has ``(extremely) poor abstractness''. Still, he continues, there are two cases where it is desirable to use phrases as denotations, e.g., for identifiers.Thus from the very beginning there has been precedent of using something other than abstract mathematical sets or domains as denotations. Even syntactic objects may be used for semantics, provided the compositionality principle is satisfied. In this paper [Eff directly in OCaml], we take as semantic objects OCaml values, equipped with

*extensional*equality. In case of functions, checking the equality involves reasoning if two OCaml functions, when applied to the same arguments, return the extensionally equal results. To be more precise, we check how the OCaml (byte-code) interpreter evaluates the applications of these functions to the same arguments. The behavior of the byte-code interpreter is well-defined; the compilation of the fragment of OCaml we are using is also well-understood (including`Obj.magic`

, which operationally is the identity). We give an example of such reasoning when justifying the adequacy of the Core delimcc semantics.Using an interpreter to define a language has long precedent, starting from (Reynolds, 1972). Such an approach was also mentioned in the survey (Schmidt, 1996):

``A pragmatist might view an operational or denotational semantics as merely an `interpreter' for a programming language. Thus, to define a semantics for a general-purpose programming language, one writes an interpreter that manipulates data structures like symbol tables (environments) and storage vectors (stores). For example, a denotational semantics for an imperative language might use an environment,`e`

, and a store,`s`

, along with an environment lookup operation,`find`

, and a storage update operation,`update`

. Since data structures like symbol tables and storage vectors are explicit, a language's subtleties are stated clearly and its flaws are exposed as awkward codings in the semantics.'' **References**- Eff Directly in OCaml

The above introduction to denotational semantics appears as Sec 3.1.4 in that paper.Peter J. Landin: The Next 700 Programming Languages

Comm. ACM, v9 N3, March 1966, pp. 157-166. doi:10.1145/365230.365257Peter D. Mosses: Denotational Semantics

In: Handbook of Theoretical Computer Science B: Formal Models and Semantics, Ed. J. van Leewen, MIT Press, 1990. Chap 11, pp. 577-631.David A. Schmidt: Programming Language Semantics

ACM Computing Surveys, v28 N1, March 1996, pp. 265-267. doi:10.1145/234313.234419,John C. Reynolds: Definitional Interpreters for Higher-Order Programming Languages

Proc. of the ACM National Conference 1972. Reprinted: Higher-Order and Symbolic Computation, v11 N4, 1998, pp. 363-397. doi:10.1023/A:1010027404223

- The language Eff is an OCaml-like language serving as a prototype
implementation of the theory of algebraic effects, intended for
experimentation with algebraic effects on a large scale.
We present the embedding of Eff into OCaml, using the library of delimited continuations or the multicore OCaml branch. The embedding is systematic, lightweight, performant and supports even higher-order, `dynamic' effects with their polymorphism. OCaml thus may be regarded as another implementation of Eff, broadening the scope and appeal of that language.

As a side contribution, we demonstrate the correctness of our embedding of Eff in OCaml denotationally, relying on the ``tagless-final'' style of interpreter-based denotational semantics. We also present the novel denotational semantics of multi-prompt delimited control that does not rely on continuation-passing-style (and is, hence, direct).

Joint work with KC Sivaramakrishnan.

**Version**- The current version is December 2018
**References**- caml-eff.pdf [746K]

The paper published in the Electronic Proceedings in Theoretical Computer Science (EPTCS), v285, 2018, pp. 23-58. doi:10.4204/EPTCS.285.2eff1.ml [10K]

Encoding of Eff in OCaml+delimcc: the code for Sections 2.2 and 4 of the paper. The code relies on the delimcc library of delimited control.queens_eff.ml [4K]

The n-queens benchmark (Sec 5 of the paper): re-casting the Eff code into OCaml, using the technique introduced in the paper. The code relies on the delimcc library of delimited control.delimcc_of_multicore.ml [3K]

delimcc interface realized in multicore OCaml: code for Sec 2.3.2 of the papermany_one.eff [5K]

Code for Sec 3.1.1 of the paper, justifying the adequacy of single-operation effects and showing the encoding of effects with multiple operationseff_semantics.ml [6K]

Core Eff in the tagless-final form and the `interpreter-based' denotational semantics of Core Eff: Sections 3.1.2 and 3.1.3 of the paperdelimcc_semantics.ml [7K]

Denotation of multiprompt delimited control: direct `interpreter-based' semantics of Core delimcc. Sec 3.2 of the papertranslation.ml [2K]

The formalization of Eff in OCaml: the translation from Core Eff to Core Delimcc, as another denotational semantics of Core Eff. Sec 3.3 of the paper then argues the two semantics are the same.Makefile [2K]

How to build and run the examples and the benchmarksThe Eff language

<http://www.eff-lang.org/>`delimcc`

: A direct implementation of delimited continuations for byte- and native-code OCaml