Journal of Logic and Computation, Volume 11, Issue 3, pp. 395-417: Abstract.
Approximation Theorems for Intersection Type Systems
Mariangiola Dezani-Ciancaglini,1, Furio Honsell2, and Yoko Motohama3
1Dipartimento di Informatica, Università di Torino, Corso Svizzera 185, 10149 Torino, Italy. E-Mail: email@example.com
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[infin] 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 [lambda]-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.
Keywords: Calculus, intersection types, approximation theorem, set-, theoretical semantics of types