WG211/M24Mosses

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 [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.