Stream Associative Nets and Lambda-mu-calculus - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2008

Stream Associative Nets and Lambda-mu-calculus

(1) , (2)
1
2
Michele Pagani
  • Function : Author
  • PersonId : 846119

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.
Fichier principal
Vignette du fichier
RR-6431.pdf (617.96 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

inria-00221221 , version 1 (28-01-2008)
inria-00221221 , version 2 (31-01-2008)
inria-00221221 , version 3 (01-02-2008)

Identifiers

  • HAL Id : inria-00221221 , version 3

Cite

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

Share

Gmail Facebook Twitter LinkedIn More