From signatures to monads in UniMath

Benedikt Ahrens 1 Ralph Matthes 2 Anders Mörtberg 3
1 ASCOLA - Aspect and composition languages
LINA - Laboratoire d'Informatique de Nantes Atlantique, Département informatique - EMN, Inria Rennes – Bretagne Atlantique
3 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
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 datatypes and their associated induction principles from other type constructors. This involves a formaliza-tion 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.
Type de document :
Pré-publication, Document de travail
2016
Liste complète des métadonnées

Littérature citée [27 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01410487
Contributeur : Anders Mortberg <>
Soumis le : mardi 6 décembre 2016 - 16:42:43
Dernière modification le : mardi 17 avril 2018 - 09:08:51
Document(s) archivé(s) le : lundi 20 mars 2017 - 17:13:38

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01410487, version 1

Citation

Benedikt Ahrens, Ralph Matthes, Anders Mörtberg. From signatures to monads in UniMath. 2016. 〈hal-01410487〉

Partager

Métriques

Consultations de la notice

224

Téléchargements de fichiers

82