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 -