Mariangiola Dezani-Ciancaglini, Furio Honsell, and Fabio Alessi. A complete characterization of complete intersection-type preorders. ACM Transactions on Computational Logic, 4(1):120-147, 2003.

We characterize those type preorders which yield complete intersection type assignment systems for lambda calculi, with respect to the thrree set-theoretical semantics for intersection types: the inference semantics, the simple semantics and the F-semantics. These semantics arise by taking as interpretation of types subsets of applicative structures, as interpretation of the preorder relation set theoretic inclusion, as interpretation of intersection constructor set theoretic intersection, and by taking as interpretation of the arrow constructor, the arrow à la Scott, with respect to either any possible functionality set, or the largest one, or the least one. These result strengthen and generalize significantly all earlier results in the literature, to ou knowledge, in at least three respects. First of all the inference semantics had not been considered before. Secondly, the characterizations are all given just in terms of simple closure conditions on the preorder relation on the types, rather than on the typing judgments themselves. The task of checking the condition is made therefore considerably more tractable. Lastly, we do not restrict attention just to lambda models, but to arbitrary applicative structures which admit an interpretation function. Thus we allow also for the treatment of models or restricted lambda calculi. Nevertheless the characterization we give can be tailored just to the case of lambda models.

[ bib | .ps ]

Back