Intersection Types and Lambda Theories

Thumbnail Image

Date

Authors

Journal Title

Journal ISSN

Volume Title

Publisher

Abstract

Description

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.

Keywords

Logic in Computer Science, F.3.2

Citation

URI

http://salesiana.dossiersoluciones.com/handle/123456789/31339

Consulte el texto completo en el siguiente enlace:

https://arxiv.org/abs/cs/0211011
 http://arxiv.org/abs/cs/0211011

Collections

arXiv