Tue 18 Jan 2022 16:30 - 16:55 at Salon III - Category Theory, HoTT, Number Theory Chair(s): Kuen-Bang Hou (Favonia)

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 Jan

Displayed 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
16:30
25m
Talk
Implementing a category-theoretic framework for typed abstract syntaxRemote
CPP
Benedikt Ahrens TU Delft, The Netherlands, Ralph Matthes IRIT, Université de Toulouse, CNRS, Toulouse INP, UT3, Toulouse, Anders Mörtberg Department of Mathematics, Stockholm University
DOI Pre-print Media Attached
16:55
25m
Talk
(Deep) Induction Rules for GADTsRemote
CPP
Patricia Johann Appalachian State University, Enrico Ghiorzi Italian Institute of Technology
Pre-print Media Attached
17:20
25m
Talk
On homotopy of walks and spherical maps in homotopy type theoryRemote
CPP
Jonathan Prieto-Cubides University of Bergen
Pre-print Media Attached
17:45
25m
Talk
Windmills of the minds: an algorithm for Fermat's Two Squares TheoremRemote
CPP
Hing Lun Chan Australian National University
DOI Pre-print Media Attached File Attached