Denotational Semantics in Agda
This project (started in 2024) aims to make it straightforward to take an existing denotational semantics of a programming language, and use Agda to check its well-formedness, as well to prove properties of individual programs.