Sciweavers

LICS
2000
IEEE
13 years 9 months ago
A Model for Impredicative Type Systems, Universes, Intersection Types and Subtyping
We introduce a new model based on coherence spaces for interpreting large impredicative type systems such as the Extended Calculus of Constructions (ECC). Moreover, we show that t...
Alexandre Miquel