From signatures to monads in UniMath

Autor: Benedikt Ahrens, Anders Mörtberg, Ralph Matthes
Přispěvatelé: University of Birmingham [Birmingham], Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, Centre National de la Recherche Scientifique (CNRS), School of Computer Science, Carnegie Mellon University, Carnegie Mellon University [Pittsburgh] (CMU), Department of Computer Science and Engineering, University of Gothenburg, Gothenburg, Sweden, Mathematical Sciences, Chalmers University of Technology and University of Gothenburg, European Project: 637339,H2020 ERC,ERC-2014-STG,CoqHoTT(2015), Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université de Toulouse (UT)-Toulouse Mind & Brain Institut (TMBI), Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT), University of Gothenburg (GU)
Jazyk: angličtina
Rok vydání: 2019
Předmět:
FOS: Computer and information sciences
Computer Science - Logic in Computer Science
Univalent mathematics
Computer science
0102 computer and information sciences
02 engineering and technology
computer.software_genre
01 natural sciences
Dependent type theory
Artificial Intelligence
Computer Science::Logic in Computer Science
0202 electrical engineering
electronic engineering
information engineering
Axiom
computer.programming_language
Recursion
Computer Science - Programming Languages
Syntax (programming languages)
Programming language
Substitution (logic)
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
020207 software engineering
Monad (functional programming)
Inductive types
Formal system
Logic in Computer Science (cs.LO)
Initial algebra semantics
Variable (computer science)
Type theory
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
Computational Theory and Mathematics
010201 computation theory & mathematics
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
Computer Science::Programming Languages
Lambda calculus
Representation of substitution
computer
Software
Programming Languages (cs.PL)
Zdroj: Journal of Automated Reasoning
Journal of Automated Reasoning, Springer Verlag, 2019, 63 (2), pp.285-318. ⟨10.1007/s10817-018-9474-4⟩
Journal of Automated Reasoning, 2019, 63 (2), pp.285-318. ⟨10.1007/s10817-018-9474-4⟩
ISSN: 0168-7433
1573-0670
DOI: 10.1007/s10817-018-9474-4⟩
Popis: 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 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\"of type theory.
Comment: 30 pages
Databáze: OpenAIRE
Externí odkaz: