Home  Online Resources  Table of Contents

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: mdezani@di.unito.it
2Dipartimento di Matematica ed Informatica, Università di Udine, Via delle Scienze 208, 33100 Udine, Italy. E-Mail: honsell@dimi.uniud.it
3Dipartimento di Informatica, Università di Torino, Corso Svizzera 185, 10149 Torino, Italy. E-Mail: yoko@di.unito.it

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

  Full-Text PDF  (282 KB)


[ Oxford University Press]   [ Oxford Journals]   [ Comments & Feedback]   Copyright© Oxford University Press, 2001.