sign in
english version rss feed

inria-00221221, version 3

Stream Associative Nets and Lambda-mu-calculus

Michele Pagani () 1, Alexis Saurin () a2

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.

 
  • inria-00221221, version 3
  • oai:hal.inria.fr:inria-00221221
  • From: 
  • Submitted on: Friday, 1 February 2008 17:48:50
  • Updated on: Saturday, 2 February 2008 11:39:30
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...