@Article{ Ah2018.1,

author = {Ahrens, Benedikt and Matthes, Ralph and Mörtberg, Anders},

title = "{From signatures to monads in UniMath}",

journal = {Journal of Automated Reasoning},

publisher = {Springer-Verlag},

address = {http://www.springerlink.com/},

year = {2018},

to_appear = {to appear},

language = {anglais},

keywords = {univalent mathematics, initial algebra semantics, inductive types, representation of substitution},

abstract = {The term UniMath refers both to a formal system for mathematics, as well as a computer-checked library of mathematics formalized in that system. The UniMath system is a core dependent type theory, augmented by the univalence axiom. The system is kept as small as possible in order to ease verification of it - in particular, general inductive types are not part of the system. In this work, we partially remedy the lack of inductive types by constructing some set-level datatypes and their associated induction principles from other type constructors. This involves a formalization of a category-theoretic result on the construction of initial algebras, as well as a mechanism to conveniently use the datatypes obtained. We also connect this construction to a previous formalization of substitution for languages with variable binding. Altogether, we construct a framework that allows us to concisely specify, via a simple notion of binding signature, a language with variable binding. From such a specification we obtain the datatype of terms of that language, equipped with a certified monadic substitution operation and a suitable recursion scheme. Using this we formalize the untyped lambda calculus and the raw syntax of Martin-Löf type theory.}

}