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.
2017
27
5
560
580
Lambda mu calculus, intersection types, approximation theorem
de' Liguoro, Ugo
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.

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