Projects per year
Abstract
We present the spinal atomic lambdacalculus, a typed lambdacalculus with explicit sharing and atomic duplication that achieves spinal full laziness: duplicating only the direct paths between a binder and bound variables is enough for beta reduction to proceed. We show this calculus is the result of a Curry–Howard style interpretation of a deepinference proof system, and prove that it has natural properties with respect to the lambdacalculus: confluence and preservation of strong normalisation.
Original language  English 

Pages  582601 
DOIs  
Publication status  Published  2020 
Fingerprint
Dive into the research topics of 'Spinal atomic lambdacalculus'. Together they form a unique fingerprint.Projects
 1 Active

Typed LambdaCalculi with Sharing and Unsharing
Engineering and Physical Sciences Research Council
1/01/19 → 30/07/22
Project: Research council