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

Bruno Barras 1, 2 Jean-Pierre Jouannaud 3 Pierre-Yves Strub 4 Qian Wang 3
2 TYPICAL - Types, Logic and computing
INRIA Saclay - Ile de France, LIX - Laboratoire d'informatique de l'école polytechnique [Palaiseau], CNRS : UMR, Polytechnique - X
3 FORMES - Formal Methods for Embedded Systems
INRIA Paris-Rocquencourt, LIAMA, Tsinghua University / Beijing
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.
Document type :
Conference papers
Twenty-Sixth Annual IEEE Symposium on "Logic in Computer Science" - LICS 2011, Jun 2011, Toronto, Canada. 2011


https://hal.inria.fr/inria-00583136
Contributor : Pierre-Yves Strub <>
Submitted on : Monday, April 4, 2011 - 9:43:34 PM
Last modification on : Wednesday, December 7, 2011 - 9:57:20 AM

File

coq-mtu-lics-2011.pdf
fileSource_public_author

Identifiers

  • HAL Id : inria-00583136, version 1

Collections

Citation

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. 2011. <inria-00583136>

Export

Share

Metrics

Consultation de
la notice

341

Téléchargement du document

106