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.
Type de document :
Communication dans un congrès
19th International Conference on Types for Proofs and Programs (TYPES 2013), Jul 2014, Toulouse, France. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 26, pp.169--187, Leibniz International Proceedings in Informatics (LIPIcs). 〈10.4230/LIPIcs.TYPES.2013.169〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01097919
Contributeur : Arnaud Spiwack <>
Soumis le : lundi 22 décembre 2014 - 16:41:47
Dernière modification le : vendredi 25 mai 2018 - 12:02:07
Document(s) archivé(s) le : lundi 23 mars 2015 - 19:25:20

Fichier

syntactic_bracket.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

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. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 26, pp.169--187, Leibniz International Proceedings in Informatics (LIPIcs). 〈10.4230/LIPIcs.TYPES.2013.169〉. 〈hal-01097919〉

Partager

Métriques

Consultations de la notice

340

Téléchargements de fichiers

101