Implementing a category-theoretic framework for typed abstract syntax
In previous work (“From signatures to monads in UniMath”), we described a category-theoretic construction of abstract syntax from a signature, mechanized in the UniMath library based on the Coq proof assistant.
In the present work, we describe what was necessary to generalize that work to account for simply-typed languages. First, some definitions had to be generalized to account for the natural appearance of non-endofunctors in the simply-typed case. As it turns out, in many cases our mechanized results carried over to the generalized definitions without any code change. Second, an existing mechanized library on 𝜔-cocontinuous functors had to be extended by constructions and theorems necessary for constructing multi-sorted syntax. Third, the theoretical framework for the semantical signatures had to be generalized from a monoidal to a bicategorical setting, again to account for non-endofunctors arising in the typed case. This uses actions of endofunctors on functors with given source, and the corresponding notion of strong functors between actions, all formalized in UniMath using a recently developed library of bicategory theory. We explain what needed to be done to plug all of these ingredients together, modularly.
The main result of our work is a general construction that, when fed with a signature for a simply-typed language, returns an implementation of that language together with suitable boilerplate code, in particular, a certified monadic substitution operation.
Tue 18 JanDisplayed time zone: Eastern Time (US & Canada) change
16:30 - 18:10
Category Theory, HoTT, Number TheoryCPP at Salon III
Chair(s): Kuen-Bang Hou (Favonia) University of Minnesota
|Implementing a category-theoretic framework for typed abstract syntaxRemote|
Benedikt Ahrens TU Delft, The Netherlands, Ralph Matthes IRIT, Université de Toulouse, CNRS, Toulouse INP, UT3, Toulouse, Anders Mörtberg Department of Mathematics, Stockholm UniversityDOI Pre-print Media Attached
|(Deep) Induction Rules for GADTsRemote|
Patricia Johann Appalachian State University, Enrico Ghiorzi Italian Institute of TechnologyPre-print Media Attached
|On homotopy of walks and spherical maps in homotopy type theoryRemote|
Jonathan Prieto-Cubides University of BergenPre-print Media Attached
|Windmills of the minds: an algorithm for Fermat's Two Squares TheoremRemote|
Hing Lun Chan Australian National UniversityDOI Pre-print Media Attached File Attached