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, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161
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.
Type de document :
Communication dans un congrès
Seventh Workshop on Logical and Semantic Frameworks, with Applications, Sep 2012, Rio de Janeiro, Brazil. 〈10.4204/EPTCS.113.5〉
Liste complète des métadonnées

Littérature citée [26 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01112158
Contributeur : Beniamino Accattoli <>
Soumis le : lundi 2 février 2015 - 13:04:48
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : dimanche 3 mai 2015 - 10:40:20

Fichiers

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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〉

Partager

Métriques

Consultations de la notice

261

Téléchargements de fichiers

96