The lazy evaluation of the λ-calculus, both in call-by-name and in call-by-value setting, is studied. Starting from a logical descriptions of two topological models of such calculi, a pre-order relation on terms, stratified by types, is defined, which grasps exactly the two operational semantics we want to model. Such a relation can be used for building two fully abstract models.

Lazy Logical Semantics

PAOLINI, LUCA LUIGI;RONCHI DELLA ROCCA, Simonetta
2004-01-01

Abstract

The lazy evaluation of the λ-calculus, both in call-by-name and in call-by-value setting, is studied. Starting from a logical descriptions of two topological models of such calculi, a pre-order relation on terms, stratified by types, is defined, which grasps exactly the two operational semantics we want to model. Such a relation can be used for building two fully abstract models.
2004
Workshop of the Italian Research Project on Computational Metamodels - COMETA Project on Computational Metamodels
Udine, Italia
15-17 december 2003
104
235
251
lazy evaluation; call-by-name; call-by-value; filter models; intersection types
L. PAOLINI; S. RONCHI DELLA ROCCA
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/28716
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? ND
social impact