Skip to Main content Skip to Navigation
Reports

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.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00221221
Contributor : Alexis Saurin <>
Submitted on : Friday, February 1, 2008 - 5:48:50 PM
Last modification on : Thursday, January 7, 2021 - 3:40:14 PM
Long-term archiving on: : Thursday, September 23, 2010 - 4:33:11 PM

Files

RR-6431.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00221221, version 3

Collections

Citation

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

Share

Metrics

Record views

476

Files downloads

289