CoqMTU: a higher-order type theory with a predicative hierarchy of universes parametrized by a decidable first-order theory - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Conference Papers Year : 2011

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

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.
Fichier principal
Vignette du fichier
coq-mtu-lics-2011.pdf (168.37 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00583136 , version 1 (04-04-2011)

Identifiers

  • HAL Id : inria-00583136 , version 1

Cite

Bruno Barras, Jean-Pierre Jouannaud, Pierre-Yves Strub, Qian Wang. CoqMTU: a higher-order type theory with a predicative hierarchy of universes parametrized by a decidable first-order theory. Twenty-Sixth Annual IEEE Symposium on "Logic in Computer Science" - LICS 2011, Jun 2011, Toronto, Canada. ⟨inria-00583136⟩
544 View
321 Download

Share

Gmail Facebook X LinkedIn More