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 de l'École normale supérieure, 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 metadatas

https://hal.inria.fr/hal-01097919
Contributor : Arnaud Spiwack <>
Submitted on : Monday, December 22, 2014 - 4:41:47 PM
Last modification on : Thursday, February 7, 2019 - 3:49:18 PM
Long-term archiving on : Monday, March 23, 2015 - 7:25:20 PM

File

syntactic_bracket.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

363

Files downloads

110