文章基本信息

标题：The Rooster and the Syntactic Bracket
本地全文：下载
作者：Hugo Herbelin ; Arnaud Spiwack
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2014
卷号：26
页码：169-187
DOI：10.4230/LIPIcs.TYPES.2013.169
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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 restrictions 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 constructions on which the Coq proof assistant is an implementation.
关键词：Coq; Calculus of inductive constructions; Impredicativity; Strictly positive type families; Inductive type families