The Atomic LambdaCalculus
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 lambdacalculus 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 lambdacalculus is an
implementation of sharing in the lambdacalculus 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
lambdacalculus. In this talk I will show how the calculus is obtained
as a CurryHoward 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.