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 this model is well-suited for interpreting intersection types and subtyping too, and we illustrate this by interpreting a variant of ECC with an additional intersection type binder. Furthermore, we propose a general method for interpreting the impredicative level in a non-syntactical way, by allowing the model to be parametrized by an arbitrarily large coherence space in order to interpret inhabitants of impredicative types. As an application, we show that uncountable types such as the type of real numbers or Zermelo-F el sets can safely be axiomatized on the impredicative level of, say, ECC, without harm for consistency.

• Type: Conference
• Year: 2000
• Where: LICS
• Authors: Alexandre Miquel
• Keywords: Automated Reasoning, Coherence Space, Interpreting, Intersection Type, LICS 2000