Mathematical Structures in Computer Science

Table of Contents - 1999 - Volume 9, Issue 05  


The call-by-value λ-calculus: a semantic investigation 1

ALBERTO PRAVATO a1, SIMONA RONCHI della ROCCA a1 and LUCA ROVERSI a2
a1 Università degli studi di Torino, Dipartimento di Informatica, C.so Svizzera 185 10149 TORINO. E-mail: pravato@di.unito.it, ronchi@di.unito.it
a2 Institut de Matématiques de Luminy, UPR 9016 – 163 Av. de Luminy – Case 907 13288 MARSEILLE Cedex 9. E-mail: rover@iml.univ-mrs.fr

Abstract

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.

(Received September 20 1996)
(Revised September 18 1998)


Footnotes

1 This work was supported by TMR-Marie Curie Grant, contract n. ERBFMBICT9601411