Abstract
Original language | English |
---|---|
Title of host publication | Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science |
Subtitle of host publication | LICS'13 |
Publisher | IEEE |
Pages | 311-320 |
Number of pages | 10 |
ISBN (Print) | 9781479904136 |
DOIs | |
Publication status | Published - 1 Aug 2013 |
Event | Twenty-Eighth Annucal ACM/IEEE Symposium on Logic in Computer Science (LICS 2013) - New Orleans, USA United States Duration: 24 Jun 2013 → 27 Jun 2013 |
Publication series
Name | ACM/IEEE Symposium on Logic in Computer Science |
---|---|
Publisher | ACM/IEEE |
ISSN (Print) | 1043-6871 |
Conference
Conference | Twenty-Eighth Annucal ACM/IEEE Symposium on Logic in Computer Science (LICS 2013) |
---|---|
Country | USA United States |
City | New Orleans |
Period | 24/06/13 → 27/06/13 |
Fingerprint
Cite this
Atomic lambda-calculus : A typed lambda-calculus with explicit sharing. / Gundersen, Tom; Heijltjes, Willem; Parigot, Michel.
Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science: LICS'13. IEEE, 2013. p. 311-320 (ACM/IEEE Symposium on Logic in Computer Science).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
}
TY - GEN
T1 - Atomic lambda-calculus
T2 - A typed lambda-calculus with explicit sharing
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 - Conference contribution
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
ER -