WG211/M24Mosses
From WG 2.11
Denotational Semantics in Agda
I recently used Agda to check the type-correctness of a denotational semantics and the soundness of some proofs about it (see [1]). One of the aims was for the definitions in Agda to correspond directly to the original definitions. This talk is about some issues that arose; addressing them might require implementing a DSL in Agda.
