We prove the confluence of λμμeT and λμμeQ, two well-behaved subcalculi of Curien and Herbelin’s λμμe calculus, stable under call-by- name and call-by-value reduction, respectively. Moreover, we study the semantics of λμμe calculus, give the interpretation of λμμeT and λμμeQ using the category of negated domains and the Kleisli category. To the best of our knowledge, this is the first interpretation of untyped λμμe calculus. We also give a thorough overview of the work on continuation semantics.
On untyped Curien-Herbelin calculus
LIKAVEC, Silvia;
2006-01-01
Abstract
We prove the confluence of λμμeT and λμμeQ, two well-behaved subcalculi of Curien and Herbelin’s λμμe calculus, stable under call-by- name and call-by-value reduction, respectively. Moreover, we study the semantics of λμμe calculus, give the interpretation of λμμeT and λμμeQ using the category of negated domains and the Kleisli category. To the best of our knowledge, this is the first interpretation of untyped λμμe calculus. We also give a thorough overview of the work on continuation semantics.File in questo prodotto:
File | Dimensione | Formato | |
---|---|---|---|
CLaC06.pdf
Accesso aperto
Tipo di file:
POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione
247.13 kB
Formato
Adobe PDF
|
247.13 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.