## Semantics of Effects

We start with simply typed lambda-calculus, with function types, sum types and product types. We look at beta and eta-laws for these types, discuss reversible derivations and the most general "positive" and "negative" connectives (this is Girard's terminology).
We add, one at a time, 3 computational effects:

- divergence (and recursion)
- printing
- storage, in a single global storage cell

We describe the **call-by-value** and **call-by-name** evaluation strategies, and discuss possible definitions of observational equivalence. Thus we have 6 languages.
We carefully establish denotational semantics for each of these 6 languages, proving soundness in each case. For call-by-value, we look at the **fine-grain call-by-value** language which simplifies the semantics. For call-by-name, we move from carrier semantics (suitable for divergence) to algebra semantics (suitable for printing) to behaviour semantics (suitable for storage).

We arrange these semantics in a table and spot the pattern: it is evident that there is a single language underlying call-by-value and call-by-name. This language is **call-by-push-value**, and we discuss its basic properties.

Paul Blain Levy
Last modified: Fri Sep 27 12:21:09 BST 2002