We consider a notion of approximation for terms of de Groote-Saurin Λμ-calculus. Then we introduce an intersection type assignment system for that calculus which is invariant under subject conversion. The type assignment system also induces a filter model, which is an extensional Λμ-model in the sense of Nakazawa and Katsumata. We then establish the approximation theorem, stating that a type can be assigned to a term in the system if and only if it can be assigned to same of its approximations.
The approximation theorem for the Λμ-calculus
DE' LIGUORO, Ugo
2017-01-01
Abstract
We consider a notion of approximation for terms of de Groote-Saurin Λμ-calculus. Then we introduce an intersection type assignment system for that calculus which is invariant under subject conversion. The type assignment system also induces a filter model, which is an extensional Λμ-model in the sense of Nakazawa and Katsumata. We then establish the approximation theorem, stating that a type can be assigned to a term in the system if and only if it can be assigned to same of its approximations.File in questo prodotto:
File | Dimensione | Formato | |
---|---|---|---|
2015 dL - The Approximation Theorem for the Lambda-Mu Calculus (preprint).pdf
Accesso aperto
Tipo di file:
PREPRINT (PRIMA BOZZA)
Dimensione
213.3 kB
Formato
Adobe PDF
|
213.3 kB | Adobe PDF | Visualizza/Apri |
deLiguoro-3-the-approximation-theorem-for-the-calculus.pdf
Accesso riservato
Tipo di file:
PDF EDITORIALE
Dimensione
208.92 kB
Formato
Adobe PDF
|
208.92 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.