DocumentCode
626298
Title
Atomic Lambda Calculus: A Typed Lambda-Calculus with Explicit Sharing
Author
Gundersen, Tom ; Heijltjes, Willem ; Parigot, Michel
Author_Institution
Univ. Paris Diderot, Paris, France
fYear
2013
fDate
25-28 June 2013
Firstpage
311
Lastpage
320
Abstract
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.
Keywords
graph theory; inference mechanisms; lambda calculus; theorem proving; type theory; Curry-Howard-style interpretation; atomic lambda-calculus; deep inference proof formalism; explicit-sharing lambda-calculus; individual constructors; lazy sharing; normalisation; optimal graph reduction; typed lambda-calculus; Calculus; Computer science; Context; Frequency modulation; Grammar; Standards; Wires;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science (LICS), 2013 28th Annual IEEE/ACM Symposium on
Conference_Location
New Orleans, LA
ISSN
1043-6871
Print_ISBN
978-1-4799-0413-6
Type
conf
DOI
10.1109/LICS.2013.37
Filename
6571563
Link To Document