This paper is about a categorical approach for modeling 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, the properties a category CC must enjoy to describe a model of call-by-value lambda-calculus are given. The category CC is general enough to catch models in Scott Domains and Coherence Spaces.
The call by value Lambda-calculus: a semantic investigation
RONCHI DELLA ROCCA, Simonetta;ROVERSI, Luca
1999-01-01
Abstract
This paper is about a categorical approach for modeling 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, the properties a category CC must enjoy to describe a model of call-by-value lambda-calculus are given. The category CC is general enough to catch models in Scott Domains and Coherence Spaces.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
PravatoRonchiRoversi1999MSCS.pdf
Accesso riservato
Tipo di file:
POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione
338.54 kB
Formato
Adobe PDF
|
338.54 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
