The call-by-value #lambda#-calculus: a semantic investigation

摘要

This paper is about a categorical approach for modelling the pure (i.e., without constants) call-by-value #lambda#-calculus, defined by Plotkin as a restriction of the call-by-name #lambda#-calculus. In particular, we give the properties that a category Cbv must enjoy to describe a model of call-by-value #lambda#-calculus. The category Cbv is general enough to catch models in Scott Domains and Coherence Spaces.