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.

• Type: Journal
• Year: 2002
• Where: CORR
• Authors: Mariangiola Dezani-Ciancaglini, Stefania Lusin
• Keywords: CORR 2002, Education, Intersection Type, Intersection Type Theory, Simple Easy Term