Categorical semantic toolset in Agda
The idea of this repository is to collect categorical tools for semantics, and for mechanized reasoning about semantics.
The underlying notion of category is chosen to be the one, implemented in the agda-categories library.
A primary focus at the moment is formalization of the concepts and results of the Higher-Order Mathematical Operational Semantics program, started in the paper: https://dl.acm.org/doi/10.1145/3571215
This project assumes the most recent version of agda-categories (i.e. the upstream main branch), which depends on version 2.0 of agda-stdlib and Agda-2.6.4.
We have supplied a flake.nix which provides a suitable environment for running this project.
The environment can be entered via
nix develop .or
direnv allowwhen using direnv
To typecheck the project, run
make agdaTo generate clickable HTML files, run
make htmlthen open meta-semantics/index.html (make open).
A somewhat recent version of the HTML output is also hosted on https://wwwcip.cs.fau.de/~hy84coky/meta-semantics/.
