An explicit-sharing lambda-calculus is presented, based on a Curry-Howard-style interpretation of the deep inference proof formalism. Duplication of subterms during reduction proceeds `atomically', i.e. on individual constructors, similar to optimal graph reduction in the style of Lamping. The calculus preserves strong normalisation with respect to the lambda-calculus, and achieves fully lazy sharing.
|Name||ACM/IEEE Symposium on Logic in Computer Science|
|Conference||Twenty-Eighth Annucal ACM/IEEE Symposium on Logic in Computer Science (LICS 2013)|
|Country/Territory||USA United States|
|Period||24/06/13 → 27/06/13|