| Intersection Types and Lambda Theories (2002) | |||||||||||||||
Abstract | |||||||||||||||
| We illustrate the use of intersection types as a semantic tool for showing properties of the lattice of l-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 l-theory: this consistency has interesting consequences on the algebraic structure of the lattice of l-theories. | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||