From Hilbert Spaces to Dilbert Spaces: Context Semantics Made Simple

摘要

We give a first-principles description of the context semantics of Gonthier, Abadi, and Levy, a computer-science analogue of Girard's geometry of interaction. We explain how this denotational semantics models A-calculus, and more generally multiplicative-exponential linear logic (MELL), by explaining the call-by-name (CBN) coding of the A-calculus, and proving the correctness of readback, where the normal form of a A-term is recovered from its semantics. This analysis yields the correctness of Lamping's optimal reduction algorithm. We relate the context semantics to linear logic types and to ideas from game semantics, used to prove full abstraction theorems for PCF and other A-calculus variants.