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

https://hal.inria.fr/hal-01112158
Contributor : Beniamino Accattoli <>
Submitted on : Monday, February 2, 2015 - 1:04:48 PM
Last modification on : Saturday, May 1, 2021 - 3:41:36 AM
Long-term archiving on: : Sunday, May 3, 2015 - 10:40:20 AM

Files

main.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

425

Files downloads

411