Fabio Alessi, Mariangiola Dezani-Ciancaglini, and Stefania
Lusin
Intersection types and domain
operators
Theoret. Comput. Sci., October 2003
to appear
We use intersection types as a tool for obtaining
lambda-models. Relying on the notion of easy intersection
type theory we successfully build a lambda-model in which the
interpretation of an arbitrary simple easy term is any filter
which can be described by a continuous predicate. This allows us
to prove two results. The first gives a proof of consistency of the lambda-theory where the
lambda-term (lambda x.xx)(lambda x.xx) is forced to behave
as the join operator. This result has interesting consequences on
the algebraic structure of the lattice of lambda-theories. The
second result is that for any simple easy term there is a
lambda-model where the interpretation of the term is the
minimal fixed point operator.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43