Projects per year
Abstract
We present the spinal atomic λcalculus, a typed λcalculus 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 λcalculus: confluence and preservation of strong normalisation.
Original language  English 

Pages  582601 
Number of pages  20 
DOIs  
Publication status  Published  2020 
Bibliographical note
Publisher Copyright:© 2020, The Author(s).
Keywords
 Curry–Howard
 Deep inference
 Full laziness
 LambdaCalculus
ASJC Scopus subject areas
 Theoretical Computer Science
 Computer Science(all)
Fingerprint
Dive into the research topics of 'Spinal atomic lambdacalculus'. Together they form a unique fingerprint.Projects
 1 Finished

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