Implementing a category-theoretic framework for typed abstract syntax

Benedikt Ahrens, Ralph Matthes, Anders Mörtberg

Research output: Chapter in Book/Report/Conference proceedingConference contribution

14 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationCPP '22
Subtitle of host publicationProceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs
EditorsAndrei Popescu, Steve Zdancewic
PublisherAssociation for Computing Machinery (ACM)
Number of pages17
ISBN (Print)9781450391825
Publication statusPublished - 17 Jan 2022
EventCPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs - Philadelphia , United States
Duration: 17 Jan 202218 Jan 2022


ConferenceCPP '22
Country/TerritoryUnited States


  • computer-checked proof
  • formalization
  • monad
  • signature
  • typed abstract syntax

ASJC Scopus subject areas

  • Computer Science Applications
  • Software


Dive into the research topics of 'Implementing a category-theoretic framework for typed abstract syntax'. Together they form a unique fingerprint.

Cite this