Formal Methods in Computing(Most of the papers antecedent to 1995are not included in the list) FRAMES  NO FRAME

 paolini02ictcs (In proceedings) Author(s) Luca Paolini Title « Call-by-Value Separability and Computability » In ICTCS'01 Series Lecture Notes in Computer Science Volume 2202 Page(s) 74--89 Year 2002 Publisher Springer, Germany ISSN number 0302-9743
 Abstract The aim of this paper is to study the notion of separability in the call-by-value 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 call-by-name setting. In the case of call-by-value $\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 call-by-value, i.e. theories in which not all terms are equal.

 BibTeX code

@inproceedings{paolini02ictcs,
volume = 2202,
issn = {0302-9743},
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 call-by-value 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
call-by-name setting. In the case of call-by-value
$\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
call-by-value, 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 = {Call-by-Value Separability and Computability},
publisher = {Springer, Germany},
pages = {74--89},
year = 2002,
}

 Formal Methods in Computing(Most of the papers antecedent to 1995are not included in the list) FRAMES  NO FRAME

This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)