## 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

*This file has been generated by
bibtex2html 1.60*
>>> BackToHomePage(Protocollo) <<<