Logic in Computer Science (LICS 2000)

Paper: A Model for Impredicative Type Systems, Universes, Intersection Types and Subtyping (at LICS 2000)

Authors: Alexandre Miquel

Abstract

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-Fränkel sets can safely be axiomatized on the impredicative level of, say, ECC, without harm for consistency.

BibTeX

  @InProceedings{Miquel-AModelforImpredicat,
    author = 	 {Alexandre Miquel},
    title = 	 {A Model for Impredicative Type Systems, Universes, Intersection Types and Subtyping},
    booktitle =  {Proceedings of the Fifteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2000},
    year =	 2000,
    editor =	 {Martin Abadi},
    month =	 {June}, 
    pages =      {18--29},
    location =   {Santa Barbara, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }