TY - GEN
T1 - Some wellfounded trees in UniMath
AU - Ahrens, Benedikt
AU - Mörtberg, Anders
PY - 2016/7/6
Y1 - 2016/7/6
N2 - UniMath, short for "Univalent Mathematics", refers to both a language (a.k.a. a formal system) for mathematics, as well as to a computer-checked library of mathematics formalized in that system. The UniMath library, under active development, aims to coherently integrate machine-checked proofs of mathematical results from many different branches of mathematics. The UniMath language is a dependent type theory, augmented by the univalence axiom. One goal is to keep the language as small as possible, to ease verification of the theory. In particular, general inductive types are not part of the language. In this work, we partially remedy this lack by constructing some inductive (families of) sets. This involves a formalization of a standard category-theoretic result on the construction of initial algebras, as well as a mechanism to conveniently use the inductive sets thus obtained. The present work constitutes one part of a construction of a framework for specifying, via a signature, programming languages with binders as nested datatypes. To this end, we are going to combine our work with previous work by Ahrens and Matthes (itself based on work by Matthes and Uustalu) on an axiomatisation of substitution for languages with variable binding. The languages specified via the framework will automatically be equipped with the structure of a monad, where the monadic operations and axioms correspond to a well-behaved substitution operation.
AB - UniMath, short for "Univalent Mathematics", refers to both a language (a.k.a. a formal system) for mathematics, as well as to a computer-checked library of mathematics formalized in that system. The UniMath library, under active development, aims to coherently integrate machine-checked proofs of mathematical results from many different branches of mathematics. The UniMath language is a dependent type theory, augmented by the univalence axiom. One goal is to keep the language as small as possible, to ease verification of the theory. In particular, general inductive types are not part of the language. In this work, we partially remedy this lack by constructing some inductive (families of) sets. This involves a formalization of a standard category-theoretic result on the construction of initial algebras, as well as a mechanism to conveniently use the inductive sets thus obtained. The present work constitutes one part of a construction of a framework for specifying, via a signature, programming languages with binders as nested datatypes. To this end, we are going to combine our work with previous work by Ahrens and Matthes (itself based on work by Matthes and Uustalu) on an axiomatisation of substitution for languages with variable binding. The languages specified via the framework will automatically be equipped with the structure of a monad, where the monadic operations and axioms correspond to a well-behaved substitution operation.
KW - Inductive datatypes
KW - Initial algebras
KW - Proof assistant
KW - UniMath
KW - Univalent type theory
UR - http://www.scopus.com/inward/record.url?scp=84978834449&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-42432-3_2
DO - 10.1007/978-3-319-42432-3_2
M3 - Conference contribution
AN - SCOPUS:84978834449
SN - 9783319424316
VL - 9725
T3 - Lecture Notes in Computer Science
SP - 9
EP - 17
BT - Mathematical Software - ICMS 2016
A2 - Greuel, Gert-Martin
A2 - Koch, Thorsten
A2 - Paule, Peter
A2 - Sommese, Andrew
PB - Springer Verlag
T2 - 5th International Conference on Mathematical Software, ICMS 2016
Y2 - 11 July 2016 through 14 July 2016
ER -