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:

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