DocumentCode :
2221500
Title :
A model for impredicative type systems, universes, intersection types and subtyping
Author :
Miquel, Alexandre
Author_Institution :
Projet Coq, Inst. Nat. de Recherche en Inf. et Autom., Le Chesnay, France
fYear :
2000
fDate :
2000
Firstpage :
18
Lastpage :
29
Abstract :
We introduce a novel 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-Frankel sets can safely be axiomatized on the impredicative level of, say, ECC, without harm for consistency
Keywords :
calculus; set theory; theorem proving; type theory; ECC; Extended Calculus of Constructions; Zermelo-Frankel sets; arbitrarily large coherence space; coherence spaces; impredicative type systems; intersection type binder; intersection types; real numbers; set axiomatization; subtyping; uncountable types; universes; Calculus; Coherence; Writing;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Logic in Computer Science, 2000. Proceedings. 15th Annual IEEE Symposium on
Conference_Location :
Santa Barbara, CA
ISSN :
1043-6871
Print_ISBN :
0-7695-0725-5
Type :
conf
DOI :
10.1109/LICS.2000.855752
Filename :
855752
Link To Document :
بازگشت