Implementing a category-theoretic framework for typed abstract syntax
Benedikt Ahrens, Ralph Matthes, Anders Mörtberg · 2022
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.