Skip to Main content Skip to Navigation
Conference papers

The Rooster and the Syntactic Bracket

Hugo Herbelin 1, 2 Arnaud Spiwack 3 
2 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
3 ANTIQUE - Analyse Statique par Interprétation Abstraite
DI-ENS - Département d'informatique - ENS Paris, Inria Paris-Rocquencourt
Abstract : We propose an extension of pure type systems with an algebraic presentation of inductive and co-inductive type families with proper indices. This type theory supports coercions toward from smaller sorts to bigger sorts via explicit type construction, as well as impredicative sorts. Type families in impredicative sorts are constructed with a bracketing operation. The necessary re-strictions of pattern-matching from impredicative sorts to types are confined to the bracketing construct. This type theory gives an alternative presentation to the calculus of inductive con-structions on which the Coq proof assistant is an implementation.
Complete list of metadata
Contributor : Arnaud Spiwack Connect in order to contact the contributor
Submitted on : Monday, December 22, 2014 - 4:41:47 PM
Last modification on : Thursday, March 17, 2022 - 10:08:44 AM
Long-term archiving on: : Monday, March 23, 2015 - 7:25:20 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License




Hugo Herbelin, Arnaud Spiwack. The Rooster and the Syntactic Bracket. 19th International Conference on Types for Proofs and Programs (TYPES 2013), Jul 2014, Toulouse, France. pp.169--187, ⟨10.4230/LIPIcs.TYPES.2013.169⟩. ⟨hal-01097919⟩



Record views


Files downloads