Hostname: page-component-745bb68f8f-cphqk Total loading time: 0 Render date: 2025-02-06T07:17:26.895Z Has data issue: false hasContentIssue false
  • English
  • Français

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

Published online by Cambridge University Press:  01 October 1999

ALBERTO PRAVATO ,
SIMONA RONCHI della ROCCA  and
LUCA ROVERSI
ALBERTO PRAVATO
Affiliation:
Università degli studi di Torino, Dipartimento di Informatica, C.so Svizzera 185 10149 TORINO. E-mail: pravato@di.unito.it, ronchi@di.unito.it
SIMONA RONCHI della ROCCA
Affiliation:
Università degli studi di Torino, Dipartimento di Informatica, C.so Svizzera 185 10149 TORINO. E-mail: pravato@di.unito.it, ronchi@di.unito.it
LUCA ROVERSI
Affiliation:
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
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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.

Type
Research Article
Information
Mathematical Structures in Computer Science , Volume 9 , Issue 5 , October 1999 , pp. 617 - 650
Copyright
1999 Cambridge University Press

Footnotes

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