query: models of CIC

• To: types@cis.upenn.edu
• Subject: query: models of CIC
• From: Milad Niqui <milad@cs.kun.nl>
• Date: Mon, 27 Oct 2003 16:45:26 +0100
• List-Archive: <http://lists.seas.upenn.edu/pipermail/types-list>
• List-Help: <mailto:types-list-request@lists.seas.upenn.edu?subject=help>
• List-Id: TYPES forum <types-list.lists.seas.upenn.edu>
• List-Post: <mailto:types-list@lists.seas.upenn.edu>
• List-Subscribe: <http://lists.seas.upenn.edu/mailman/listinfo/types-list>, <mailto:types-list-request@lists.seas.upenn.edu?subject=subscribe>
• List-Unsubscribe: <http://lists.seas.upenn.edu/mailman/listinfo/types-list>, <mailto:types-list-request@lists.seas.upenn.edu?subject=unsubscribe>
• Sender: types-list-bounces+bcpierce=cis.upenn.edu@lists.seas.upenn.edu
• User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-GB; rv:1.4) Gecko/20030703

[----- 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).

Regards,

-- 
Milad Niqui

Computing Science Department,                tel:+31 24 365 2631
University of Nijmegen,                      fax:+31 24 365 2525
P.O.B. 9010,                                 email: milad@cs.kun.nl
6500 GL Nijmegen,                            http://www.cs.kun.nl/~milad
The Netherlands.

• Prev: Subject: CFP: Computer Aided Verification (CAV) 2004, Boston, MA
• Next: query: models of CIC
• Index(es):
  • Main
  • Thread