paolini02ictcs (In proceedings)

Author(s)  Luca Paolini 
Title  « CallbyValue Separability and Computability » 
In  ICTCS'01 
Series  Lecture Notes in Computer Science 
Volume  2202 
Page(s)  7489 
Year  2002 
Publisher  Springer, Germany 
ISSN number  03029743 
Abstract 
The aim of this paper is to study the notion of separability in the callbyvalue setting. Separability is the key notion used in the Böhm theorem, proving that syntactically different $\beta $normal forms are separable in the classical $\lambda $calculus endowed with $\beta $reduction, i.e. in the callbyname setting. In the case of callbyvalue $\lambda $calculus endowed with $\beta $_{v}reduction and $\beta $_{v}reduction, it turns out that two syntactically different $\beta \eta $normal forms are separable too, while the notions of $\beta $_{v}normal form and $\beta $_{v}normal form are semantically meaningless. An explicit representation of Kleenes recursive functions is presented. The separability result guarantees that the representation makes sense in every consistent theory of callbyvalue, i.e. theories in which not all terms are equal. 
Download the complete article:
@inproceedings{paolini02ictcs,
volume = 2202,
issn = {03029743},
author = {Luca Paolini},
series = {Lecture Notes in Computer Science},
booktitle = {ICTCS'01},
abstract = {The aim of this paper is to study the notion of separability in
the callbyvalue setting. Separability is the key notion used in
the B\"ohm theorem, proving that syntactically different
$\beta$normal forms are separable in the classical
$\lambda$calculus endowed with $\beta$reduction, i.e. in the
callbyname setting. In the case of callbyvalue
$\lambda$calculus endowed with $\beta_v$reduction and
$\beta_v$reduction, it turns out that two syntactically different
$\beta\eta$normal forms are separable too, while the notions of
$\beta_v$normal form and $\beta_v$normal form are semantically
meaningless. An explicit representation of Kleenes recursive
functions is presented. The separability result guarantees that
the representation makes sense in every consistent theory of
callbyvalue, i.e. theories in which not all terms are equal.},
localfile = {http://www.di.unito.it/~paolini/papers/cbv_separability.pdf},
tag = {7th Italian Conference in Theoretical Computer Science},
title = {CallbyValue Separability and Computability},
publisher = {Springer, Germany},
pages = {7489},
year = 2002,
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)