Stream Associative Nets and Lambda-mu-calculus

Michele Pagani 1 Alexis Saurin 2
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : $\Lambda\mu$-calculus has been built as an untyped extension of Parigot's $\lambda\mu$-calculus in order to recover Böhm theorem which was known to fail in $\lambda\mu$-calculus. An essential computational feature of $\Lambda\mu$-calculus for separation to hold is the unrestricted use of abstractions over continuations that provides the calculus with a construction of streams. Based on the Curry-Howard paradigm Laurent has defined a translation of $\Lambda\mu$-calculus in polarized proof-nets. Unfortunately, this translation cannot be immediately extended to $\Lambda\mu$-calculus: the type system on which it is based freezes \Lm-calculus's stream mechanism. We introduce \emph{stream associative nets (SANE)}, a notion of nets which is between Laurent's polarized proof-nets and the usual linear logic proof-nets. SANE have two kinds of $\lpar$ (hence of $\ltens$), one is linear while the other one allows free structural rules (as in polarized proof-nets). We prove confluence for SANE and give a reduction preserving encoding of $\Lambda\mu$-calculus in SANE, based on a new type system introduced by the second author. It turns out that the stream mechanism at work in $\Lambda\mu$-calculus can be explained by the associativity of the two different kinds of $\lpar$ of SANE. At last, we achieve a Böhm theorem for SANE. This result follows Girard's program to put into the fore the separation as a key property of logic.
Type de document :
[Research Report] RR-6431, INRIA. 2008, pp.48
Liste complète des métadonnées
Contributeur : Alexis Saurin <>
Soumis le : vendredi 1 février 2008 - 17:48:50
Dernière modification le : jeudi 15 novembre 2018 - 20:26:59
Document(s) archivé(s) le : jeudi 23 septembre 2010 - 16:33:11


Fichiers produits par l'(les) auteur(s)


  • HAL Id : inria-00221221, version 3



Michele Pagani, Alexis Saurin. Stream Associative Nets and Lambda-mu-calculus. [Research Report] RR-6431, INRIA. 2008, pp.48. 〈inria-00221221v3〉



Consultations de la notice


Téléchargements de fichiers