2002/11/12 by M. Dezani-Ciancaglini, Dezani-Ciancaglini, M., S. Lusin +1
Computer Science · #F.3.2 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #cs.LO
paper · pdf · doi:10.48550/arxiv.cs/0211011
arxiv created 2002/11/12 · arxiv updated 2009/11/30
We illustrate the use of intersection types as a semantic tool for showing properties of the lattice of lambda 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 predicate. This allows us to prove the consistency of a well-know lambda theory: this consistency has interesting consequences on the algebraic structure of the lattice of lambda theories.