inria-00221221, version 3
Stream Associative Nets and Lambda-mu-calculus
Michele Pagani
1Alexis Saurin
a, 2
N° RR-6431 (2008)
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.
- a – Polytechnique - X
- 1: Preuves, Programmes et Systèmes (PPS)
- CNRS : UMR7126 – Université Paris VII - Paris Diderot
- 2: PARSIFAL (INRIA Futurs)
- CNRS : UMR7161 – INRIA – Polytechnique - X
- Domain : Computer Science/Logic in Computer Science
- Internal note : RR-6431
- Available versions : v1 (2008-01-28) v2 (2008-01-31) v3 (2008-02-02)
- inria-00221221, version 3
- http://hal.inria.fr/inria-00221221
- oai:hal.inria.fr:inria-00221221
- From: Alexis Saurin
- Submitted on: Friday, 1 February 2008 17:48:50
- Updated on: Saturday, 2 February 2008 11:39:30






Associated documents

Export