A lambda-calculus that achieves full laziness with spine duplication

Abstract

This work introduces a variant of Gundersen, Heijltjes, and Parigot’s atomic lambda calculus. This typeable calculus with explicit sharing extends the Curry-Howard interpretation of open deduction already established by the mentioned. We extend the intuitionisitc proof system with a switch inference rule, which corresponds to an end-of-scope operator i.e. the switch rule can only be applied to subterms of an abstraction that do not have the binding variable occuring freely inside. Combining this notion of scope with the previous calculus, where duplication of terms is performed atomically, results in the ability to duplicate the spine of an abstraction, where the spine is the direct path from the binder to the bound variable. Spine duplication has been witnessed previously with strategies involving graphs and labels, but this work uses environments and remains in a typed setting. We prove that this calculus preserves strong normalisation with respect to the lambda calculus, satisfies the confluence property, and can duplicate the spine on any abstraction.

Date of Award	4 Sept 2019
Original language	English
Supervisor	Alessio Guglielmi (Supervisor) & Willem Heijltjes (Supervisor)