Proof-Nets and the Call-by-Value Lambda-Calculus - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2012

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

Résumé

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.
Fichier principal
Vignette du fichier
main.pdf (230.99 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01112158 , version 1 (02-02-2015)

Identifiants

Citer

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⟩
174 Consultations
185 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More