On Friday October 17, this site was moved to a new server, https://mw.hh.se. The original address will continue to work. Whithin a week or two this site will return to the original address. /Peo HH IT-dep

WG211/M24Mosses

From WG 2.11
Revision as of 15:17, 22 November 2024 by Peter (talk | contribs) (Initial version.)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search

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.

Retrieved from "http://mw.hh.se/wg211/index.php?title=WG211/M24Mosses&oldid=2672"