To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

From Signatures to Monads… - University of Gothenburg, Sweden Till startsida
Sitemap
To content Read more about how we use cookies on gu.se

From Signatures to Monads in UniMath

Journal article
Authors B. Ahrens
R. Matthes
Anders Mörtberg
Published in Journal of Automated Reasoning
Volume 63
Issue 2
Pages 285-318
ISSN 0168-7433
Publication year 2019
Published at Department of Computer Science and Engineering, Computing Science, Programming Logic
Pages 285-318
Language en
Links dx.doi.org/10.1007/s10817-018-9474-...
Keywords Univalent mathematics, Initial algebra semantics, Inductive types, Representation of substitution, inductive types, substitution, syntax, Computer Science
Subject categories Computer and Information Science

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-Lof type theory.

Page Manager: Webmaster|Last update: 9/11/2012
Share:

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?