In this paper we prove that many intersection type theories of interest (including those which induce as filter models, Scott's and Park's D∞ models, the models studied in Barendregt Coppo Dezani, Abramsky Ong, and Honsell Ronchi) satisfy an Approximation Theorem with respect to a suitable notion of approximant. This theorem implies that a λ-term has a type if and only if there exists an approximant of that term which has that type. We prove this result uniformly for all the intersection type theories under consideration using a Kripke version of stable sets where bases correspond to worlds.

Approximation Theorems for intersection type systems

HONSELL, Furio;MOTOHAMA, Yoko
2001

Abstract

In this paper we prove that many intersection type theories of interest (including those which induce as filter models, Scott's and Park's D∞ models, the models studied in Barendregt Coppo Dezani, Abramsky Ong, and Honsell Ronchi) satisfy an Approximation Theorem with respect to a suitable notion of approximant. This theorem implies that a λ-term has a type if and only if there exists an approximant of that term which has that type. We prove this result uniformly for all the intersection type theories under consideration using a Kripke version of stable sets where bases correspond to worlds.
File in questo prodotto:
File Dimensione Formato  
J Logic Computation-2001-Dezani-Ciancaglini-395-417.pdf

non disponibili

Tipologia: Documento in Post-print
Licenza: Non pubblico
Dimensione 276.35 kB
Formato Adobe PDF
276.35 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: http://hdl.handle.net/11390/675452
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 4
  • ???jsp.display-item.citation.isi??? 3
social impact