The call-by-value λ-calculus: a semantic investigation This work was supported by TMR-Marie Curie Grant, contract n. ERBFMBICT9601411
PRAVATO, ALBERTO; della ROCCA, SIMONA RONCHI; ROVERSI, LUCA; PRAVATO ALBERTO; Università degli studi di Torino; della ROCCA SIMONA RONCHI; Università degli studi di Torino; ROVERSI LUCA; Institut de Matématiques de Luminy
Журнал:
Mathematical Structures in Computer Science
Дата:
1999
Аннотация:
This paper is about a categorical approach for modelling the pure (i.e., without constants) call-by-value λ-calculus, defined by Plotkin as a restriction of the call-by-name λ-calculus. In particular, we give the properties that a category Cbv must enjoy to describe a model of call-by-value λ-calculus. The category Cbv is general enough to catch models in Scott Domains and Coherence Spaces.
476.8Кб