The call-by-value λ-calculus: a semantic investigation
Alberto Pravato, Simona Ronchi Della Rocca, Luca Roversi · 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.