Subtyping in first order object calculi is studied with respect to the logical semantics obtained by identifying terms that satisfy the same set of predicates, as formalised through an assignment system. It is shown that equality in the full first order sigma-calculus is modelled by this notion, which in turn is included in a Morris-style contextual equivalence.
Logical equivalence for subtyping and recursive types
DE' LIGUORO, Ugo
2008-01-01
Abstract
Subtyping in first order object calculi is studied with respect to the logical semantics obtained by identifying terms that satisfy the same set of predicates, as formalised through an assignment system. It is shown that equality in the full first order sigma-calculus is modelled by this notion, which in turn is included in a Morris-style contextual equivalence.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
vBdL08.pdf
Accesso riservato
Tipo di file:
POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione
1.63 MB
Formato
Adobe PDF
|
1.63 MB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
