Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Fifteenth Annual IEEE Symposium on

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 Symposium on Logic in Computer Science (LICS 2000)},
    year =	 {2000},
    month =	 {June}, 
    pages =      {18--29},
    location =   {Santa Barbara, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski