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

Bruno Barras; Jean-Pierre Jouannaud; Pierre-Yves Strub; Qian Wang

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 () ^1, 2, Jean-Pierre Jouannaud () ³, Pierre-Yves Strub () ⁴, Qian Wang () ³

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.

1: Laboratoire d'informatique de l'école polytechnique (LIX)
CNRS : UMR7161 – Polytechnique - X
2: TYPICAL (INRIA Saclay - Ile de France)
INRIA – CNRS : UMR – Polytechnique - X
3: FORMES (LIAMA)
INRIA – Tsinghua University / Beijing – LIAMA
4: Microsoft Research - Inria Joint Centre (MSR - INRIA)
INRIA – Microsoft – Microsoft Research Laboratory Cambridge

inria-00583136, version 1
http://hal.inria.fr/inria-00583136
oai:hal.inria.fr:inria-00583136
From: Pierre-Yves Strub <>
Submitted on: Monday, 4 April 2011 21:43:34
Updated on: Wednesday, 7 December 2011 09:57:20

See detailed view

Associated documents

PDF :

Export

Bibtex EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="inproceedings"><head>Peer-reviewed conferences/proceedings</head>
<biblStruct type="inproceedings" xml:id="inria-00583136"><analytic>
<author><persName><forename>Bruno</forename><surname>Barras</surname></persName>
<affiliation>
<orgName type="laboratory">LIX</orgName>
<orgName type="team">Laboratoire d'informatique de l'école polytechnique</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR7161</orgName>
<orgName type="institution">Polytechnique - X</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">INRIA Saclay - Ile de France</orgName>
<orgName type="team">TYPICAL</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR</orgName>
<orgName type="institution">Polytechnique - X</orgName>
</affiliation>
</author>
<author><persName><forename>Jean-Pierre</forename><surname>Jouannaud</surname></persName>
<affiliation>
<orgName type="laboratory">LIAMA</orgName>
<orgName type="team">FORMES</orgName>
<country>CN</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">Tsinghua University / Beijing</orgName>
<orgName type="institution">LIAMA</orgName>
</affiliation>
</author>
<author><persName><forename>Pierre-Yves</forename><surname>Strub</surname></persName>
<affiliation>
<orgName type="laboratory">MSR - INRIA</orgName>
<orgName type="team">Microsoft Research - Inria Joint Centre</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">Microsoft</orgName>
<orgName type="institution">Microsoft Research Laboratory Cambridge</orgName>
</affiliation>
</author>
<author><persName><forename>Qian</forename><surname>Wang</surname></persName>
<affiliation>
<orgName type="laboratory">LIAMA</orgName>
<orgName type="team">FORMES</orgName>
<country>CN</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">Tsinghua University / Beijing</orgName>
<orgName type="institution">LIAMA</orgName>
</affiliation>
</author>
<title type="main" level="a">CoqMTU: a higher-order type theory with a predicative hierarchy of universes parametrized by a decidable first-order theory</title></analytic><monogr><meeting>Twenty-Sixth Annual IEEE Symposium on "Logic in Computer Science" - LICS 2011</meeting><imprint><pubPlace><settlement>Toronto</settlement><country>Canada</country></pubPlace><biblScope type="publicationDate">2011-00-00</biblScope></imprint></monogr><idno type="HALid">http://hal.inria.fr/inria-00583136</idno><idno type="HALFile">http://hal.inria.fr/inria-00583136/PDF/coq-mtu-lics-2011.pdf</idno></biblStruct>
</listBibl>
</listBibl>