M. Dezani-Ciancaglini and S. Lusin
Intersection types and lambda
theories
In WIT 2002, 2002
We illustrate the use of intersection types as a
semantic tool
for showing properties of the lattice of lambda
theories. Relying
on the notion of easy intersection type theory
we successfully
build a filter model in which the interpretation
of an arbitrary
simple easy term is any filter which can be
described in an
uniform way by a recursive predicate. This
allows us to prove
the consistency of a well-know lambda theory:
this consistency
has interesting consequences on the algebraic
structure of the
lattice of lambda theories.
[ bib |
http |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43