``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 judgment like a jigsaw
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 thereof, 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 - Not by Equations Alone: Reasoning with Extensible Effects

How denotational semantics can be used to reason and optimize interesting programs with non-determinism and state. For the first time, precisely specified what*equivalence modulo handlers*(`modulo observation') really means and proved it to be congruence - 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 - Elementary Tutorial on Normalization-by-Evaluation
- 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 - Executable denotational semantics of code generation with let rec insertion
- Reference-type variables vs. mutable variables
- Free Variables and Free Effects: two different ways of denoting terms with free variables
- 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 challenge of reasoning about programs with (multiple) effects
such as mutation, jumps or IO dates back to the inception of program
semantics in the works of Strachey and Landin. Using monads to
represent individual effects and the associated equational laws to
reason about them proved exceptionally effective. Even then it is
not always clear what laws are to be associated with a monad -- for
a good reason, as we show for non-determinism. Combining expressions
using different effects brings challenges not just for monads, which
do not compose, but also for equational reasoning: the interaction
of effects may invalidate their individual laws, as well as induce
emerging properties that are not apparent in the semantics of
individual effects. Overall, the problems are judging the adequacy
of a law; determining if or when a law continues to hold upon
addition of new effects; and obtaining and easily verifying emergent
laws.
We present a solution relying on the framework of (algebraic, extensible) effects, which already proved itself for writing programs with multiple effects. Equipped with a fairly conventional denotational semantics, this framework turns useful, as we demonstrate, also for reasoning about and optimizing programs with multiple interacting effects. Unlike the conventional approach, equational laws are not imposed on programs/effect handlers, but induced from them: our starting point hence is a program (model), whose denotational semantics, besides being used directly, suggests and justifies equational laws and clarifies side-conditions. The main technical result is the introduction of the notion of

*equivalence modulo handlers*(`modulo observation') or a particular combination of handlers -- and proving it to be a*congruence*. It is hence usable for reasoning in any context, not just evaluation contexts -- provided particular conditions are met.Concretely, we describe several realistic handlers for non-determinism and elucidate their laws (some of which hold in the presence of any other effect). We demonstrate appropriate equational laws of non-determinism in the presence of global state, which have been a challenge to state and prove before.

In short, the paper is about:

- Reasoning about programs with several effects: in particular, non-determinism and state
- Equational laws modulo handler (modulo observation),
*as congruence*, shown for the first time - Determining what, after all, are the laws of non-determinism, as used in practice
- Many examples of reasoning about global state and non-determinism, proving many particular, emergent laws
- Contra: checking a handler satisfying an equational theory
- Contra: combining equational theories
- Contra: semi-lattice laws of non-determinism

Although the paper at times uses heavy machinery, the main ideas are explained in Section 2 on mere addition.

Joint work with Shin-Cheng Mu and Amr Sabry.

**Version**- The current version is December 2020
**References**- denot.pdf [503K]

The paper published in Journal of Functional Programming, v. 31, 2021, e2 doi:10.1017/S0956796820000271DSL of algebraic effects and handlers

The implementation of the calculus. It is used to run all the examples in the paper. Thus, the equational laws discussed in the paper are not only proven but also tested.

- 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 multiprompt 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