Intersection Types and Lambda Theories

8 years 8 months ago
Intersection Types and Lambda Theories
We illustrate the use of intersection types as a semantic tool for showing properties of the lattice of -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 -theory: this consistency has interesting consequences on the algebraic structure of the lattice of -theories.
Mariangiola Dezani-Ciancaglini, Stefania Lusin
Added 19 Dec 2010
Updated 19 Dec 2010
Type Journal
Year 2002
Where CORR
Authors Mariangiola Dezani-Ciancaglini, Stefania Lusin
Comments (0)