Skip to Main content Skip to Navigation
Conference papers

Proof-Nets and the Call-by-Value Lambda-Calculus

Beniamino Accattoli 1, 2 
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : This paper gives a detailed account of the relationship between (a variant of) the call-by-value lambda calculus and linear logic proof nets. The presentation is carefully tuned in order to realize a strong bisimulation between the two systems: every single rewriting step on the calculus maps to a single step on the nets, and viceversa. In this way, we obtain an algebraic reformulation of proof nets. Moreover, we provide a simple correctness criterion for our proof nets, which employ boxes in an unusual way.
Document type :
Conference papers
Complete list of metadata

Cited literature [26 references]  Display  Hide  Download
Contributor : Beniamino Accattoli Connect in order to contact the contributor
Submitted on : Monday, February 2, 2015 - 1:04:48 PM
Last modification on : Saturday, June 25, 2022 - 9:09:22 PM
Long-term archiving on: : Sunday, May 3, 2015 - 10:40:20 AM


Files produced by the author(s)




Beniamino Accattoli. Proof-Nets and the Call-by-Value Lambda-Calculus. Seventh Workshop on Logical and Semantic Frameworks, with Applications, Sep 2012, Rio de Janeiro, Brazil. ⟨10.4204/EPTCS.113.5⟩. ⟨hal-01112158⟩



Record views


Files downloads