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 -