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
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;
Conference_Titel :
Logic in Computer Science (LICS), 2013 28th Annual IEEE/ACM Symposium on
Conference_Location :
New Orleans, LA
Print_ISBN :
978-1-4799-0413-6
DOI :
10.1109/LICS.2013.37
