Skip to main content

The Atomic Lambda-Calculus

Willem Heijltjes ( University of Bath )

 

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.

Speaker bio

Willem Heijltjes is Prize Fellow in Computer Science at the University of Bath. He previously held a post-doctoral position in Ecole Polytechnique, Paris, after completing a PhD at the University of Edinburgh. The main emphasis of his work is on graphical approaches to proof and computation, such as proof nets for linear and classical logic.

Share this: