sign in
english version rss feed

inria-00583136, version 1

CoqMTU: a higher-order type theory with a predicative hierarchy of universes parametrized by a decidable first-order theory

Bruno Barras () 12, Jean-Pierre Jouannaud () 3, Pierre-Yves Strub () 4, Qian Wang () 3

Twenty-Sixth Annual IEEE Symposium on "Logic in Computer Science" - LICS 2011 (2011)

Abstract: We study a complex type theory, a Calculus of Inductive Constructions with a predicative hierarchy of universes and a first-order theory T built in its conversion relation. The theory T is specified abstractly, by a set of constructors, a set of defined symbols, axioms expressing that constructors are free and defined symbols completely defined, and a generic elimination principle relying on crucial properties of first-order structures satisfying the axioms. We first show that CoqMTU enjoys all basic meta-theoretical properties of such calculi, confluence, subject reduction and strong normalization when restricted to weak-elimination, implying the decidability of type-checking in this case as well as consistency. The case of strong elimination is left open.

  • Domain : Computer Science/Logic in Computer Science
 
  • inria-00583136, version 1
  • oai:hal.inria.fr:inria-00583136
  • From: 
  • Submitted on: Monday, 4 April 2011 21:43:34
  • Updated on: Wednesday, 7 December 2011 09:57:20
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...