TY - GEN

T1 - Atomic lambda-calculus

T2 - Twenty-Eighth Annucal ACM/IEEE Symposium on Logic in Computer Science (LICS 2013)

AU - Gundersen, Tom

AU - Heijltjes, Willem

AU - Parigot, Michel

PY - 2013/8/1

Y1 - 2013/8/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84883443813&partnerID=8YFLogxK

UR - http://lii.rwth-aachen.de/lics/lics13/

UR - http://dx.doi.org/10.1109/LICS.2013.37

U2 - 10.1109/LICS.2013.37

DO - 10.1109/LICS.2013.37

M3 - Chapter in a published conference proceeding

AN - SCOPUS:84883443813

SN - 9781479904136

T3 - ACM/IEEE Symposium on Logic in Computer Science

SP - 311

EP - 320

BT - Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science

PB - IEEE

Y2 - 24 June 2013 through 27 June 2013

ER -