The Atomic Lambda-Calculus
Willem Heijltjes ( University of Bath )
- 14:00 14th October 2014 ( week 1, Michaelmas Term 2014 )Lecture Theatre B
The key to efficient implementation of the lambda-calculus is sharing:
using a single stored term to represent many similar ones, and computing
with it once, instead of computing on each instance. This is the
principle behind explicit substitution calculi, labelled calculi,
sharing graphs, and related formalisms. The atomic lambda-calculus is an
implementation of sharing in the lambda-calculus that exhibits a unique
combination of features. It is a typed term calculus that implements
duplication atomically, one constructor at a time. The calculus achieves
fully lazy sharing, and preserves strong normalisation w.r.t. the
lambda-calculus. In this talk I will show how the calculus is obtained
as a Curry-Howard interpretation of intuitionistic logic in deep
inference, a family of proof systems in which atomicity is a typical
feature. This is joint work with Tom Gundersen and Michel Parigot.