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

paolini02ictcs (In proceedings)
Author(s) Luca Paolini
Title« Call-by-Value Separability and Computability »
InICTCS'01
SeriesLecture Notes in Computer Science
Volume2202
Page(s)74--89
Year2002
PublisherSpringer, Germany
ISSN number0302-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 β-normal forms are separable in the classical λ-calculus endowed with β-reduction, i.e. in the call-by-name setting. In the case of call-by-value λ-calculus endowed with βv-reduction and βv-reduction, it turns out that two syntactically different βη-normal forms are separable too, while the notions of βv-normal form and β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.

Download the complete article: cbv_separability.pdf

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,
}


 Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are 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)

Valid HTML 4.01!