Fabio Alessi, Mariangiola Dezani-Ciancaglini, and Stefania
Lusin
Intersection types and domain
operators
Theoret. Comput. Sci., 316(1-3):25-47, 2004
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