Some wellfounded trees in UniMath

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Authors

Colleges, School and Institutes

External organisations

  • Institute for Advanced Study, Princeton, NJ, USA

Abstract

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.

Details

Original languageEnglish
Title of host publicationMathematical Software - ICMS 2016
Subtitle of host publication5th International Conference, Berlin, Germany, July 11-14, 2016, Proceedings
EditorsGert-Martin Greuel, Thorsten Koch, Peter Paule, Andrew Sommese
Publication statusPublished - 6 Jul 2016
Event5th International Conference on Mathematical Software, ICMS 2016 - Berlin, Germany
Duration: 11 Jul 201614 Jul 2016

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume9725
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference5th International Conference on Mathematical Software, ICMS 2016
CountryGermany
CityBerlin
Period11/07/1614/07/16

Keywords

  • Inductive datatypes, Initial algebras, Proof assistant, UniMath, Univalent type theory