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

doi:10.1109/LICS.2011.37

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	Proceedings - 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	143-151
Number of pages	9
ISBN (Print)	9780769544120
DOIs	https://doi.org/10.1109/LICS.2011.37
Publication status	Published - 1 Jan 2011
Externally published	Yes

Publication series

Name	Proceedings - Symposium on Logic in Computer Science
ISSN (Print)	1043-6871

Access to Document

10.1109/LICS.2011.37

Cite this

Barras, B., Jouannaud, J. P., Strub, P. Y., & Wang, Q. (2011). COQMTU: A higher-order type theory with a predicative hierarchy of universes parametrized by a decidable first-order theory. In Proceedings - 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011 (pp. 143-151). Article 5970212 (Proceedings - Symposium on Logic in Computer Science). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/LICS.2011.37

Barras, Bruno ; Jouannaud, Jean Pierre ; Strub, Pierre Yves et al. / COQMTU : A higher-order type theory with a predicative hierarchy of universes parametrized by a decidable first-order theory. Proceedings - 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011. Institute of Electrical and Electronics Engineers Inc., 2011. pp. 143-151 (Proceedings - Symposium on Logic in Computer Science).

@inproceedings{e2bcdc41302e4b50902594b054b43289,

title = "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.",

author = "Bruno Barras and Jouannaud, \{Jean Pierre\} and Strub, \{Pierre Yves\} and Qian Wang",

year = "2011",

month = jan,

day = "1",

doi = "10.1109/LICS.2011.37",

language = "English",

isbn = "9780769544120",

series = "Proceedings - Symposium on Logic in Computer Science",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "143--151",

booktitle = "Proceedings - 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011",

}

Barras, B, Jouannaud, JP, Strub, PY & Wang, Q 2011, COQMTU: A higher-order type theory with a predicative hierarchy of universes parametrized by a decidable first-order theory. in Proceedings - 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011., 5970212, Proceedings - Symposium on Logic in Computer Science, Institute of Electrical and Electronics Engineers Inc., pp. 143-151. https://doi.org/10.1109/LICS.2011.37

COQMTU: A higher-order type theory with a predicative hierarchy of universes parametrized by a decidable first-order theory. / Barras, Bruno; Jouannaud, Jean Pierre; Strub, Pierre Yves et al.
Proceedings - 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011. Institute of Electrical and Electronics Engineers Inc., 2011. p. 143-151 5970212 (Proceedings - Symposium on Logic in Computer Science).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - COQMTU

T2 - A higher-order type theory with a predicative hierarchy of universes parametrized by a decidable first-order theory

AU - Barras, Bruno

AU - Jouannaud, Jean Pierre

AU - Strub, Pierre Yves

AU - Wang, Qian

PY - 2011/1/1

Y1 - 2011/1/1

N2 - 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.

AB - 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.

U2 - 10.1109/LICS.2011.37

DO - 10.1109/LICS.2011.37

M3 - Conference contribution

AN - SCOPUS:80052160838

SN - 9780769544120

T3 - Proceedings - Symposium on Logic in Computer Science

SP - 143

EP - 151

BT - Proceedings - 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011

PB - Institute of Electrical and Electronics Engineers Inc.

ER -

Barras B, Jouannaud JP, Strub PY, Wang Q. COQMTU: A higher-order type theory with a predicative hierarchy of universes parametrized by a decidable first-order theory. In Proceedings - 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011. Institute of Electrical and Electronics Engineers Inc. 2011. p. 143-151. 5970212. (Proceedings - Symposium on Logic in Computer Science). doi: 10.1109/LICS.2011.37

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

Abstract

Publication series

Access to Document

Fingerprint

Cite this