Bibtex de la publication

@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},
volume = {62},
pages = {1--34},
language = {anglais},
URL = {https://doi.org/10.1007/s10817-018-9474-4},
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.}
}