Till sidans topp

Sidansvarig: Webbredaktion
Sidan uppdaterades: 2012-09-11 15:12

Tipsa en vän
Utskriftsversion

From Signatures to Monads… - Göteborgs universitet Till startsida
Webbkarta
Till innehåll Läs mer om hur kakor används på gu.se

From Signatures to Monads in UniMath

Artikel i vetenskaplig tidskrift
Författare B. Ahrens
R. Matthes
Anders Mörtberg
Publicerad i Journal of Automated Reasoning
Volym 63
Nummer/häfte 2
Sidor 285-318
ISSN 0168-7433
Publiceringsår 2019
Publicerad vid Institutionen för data- och informationsteknik, datavetenskap, programmeringslogik (GU)
Sidor 285-318
Språk en
Länkar dx.doi.org/10.1007/s10817-018-9474-...
Ämnesord Univalent mathematics, Initial algebra semantics, Inductive types, Representation of substitution, inductive types, substitution, syntax, Computer Science
Ämneskategorier Data- och informationsvetenskap

Sammanfattning

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.

Sidansvarig: Webbredaktion|Sidan uppdaterades: 2012-09-11
Dela:

På Göteborgs universitet använder vi kakor (cookies) för att webbplatsen ska fungera på ett bra sätt för dig. Genom att surfa vidare godkänner du att vi använder kakor.  Vad är kakor?