query: models of CIC
[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
Dear Type Community,
Is there a realizability semantics or set theoretical model known for
CIC (i.e. Calculus of Inductive Contrsuctions, the underlying type
theory of Coq proof assistant)? In CIC we have two impredicative
universes,Prop and Set and a cumulative hierarchy of Type_0, Type_1, ...
on top of them. Moreover we have (dependent) inductive types both on the
predicative and the impredicative level and we have dependent
elimination on Set (which is stronger than the one for Prop).
Computing Science Department, tel:+31 24 365 2631
University of Nijmegen, fax:+31 24 365 2525
P.O.B. 9010, email: email@example.com
6500 GL Nijmegen, http://www.cs.kun.nl/~milad