From Hilbert Spaces to Dilbert Spaces: Context Semantics Made Simple

Abstract

Context semantics is a computer-science analogue of Girard's geometry of interaction, which was designed to give a denotational meaning to proofs in linear logic. Its interest to computer scientists, among its other virtues, is that it gives a sequential meaning to functional programming languages with higher-order types. I'll explain how this denotational semantics models lambda calculus and PCF, which are both simple, mathematically idealized versions of Lisp. In particular, I'll discuss readback, where the normal form (fully evaluated structure) of a program can be recovered from its semantics. This analysis can be used to prove the correctness of optimal evaluation algorithms which maximize the sharing of computations. If you have seen Lisp or a functional programming language, you'll know what I'm talking about. My presentation doesn't have a lot of theorems, but it does have a lot of nice looking pictures.