**Speaker**: Harry Mairson

Computer Science Department and

Volen Center for Complex Numbers

Brandeis University

**Title**: 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.