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: Difference between revisions
From WG 2.11
Jump to navigationJump to search
Initial version. |
Added the heading. |
||
| Line 1: | Line 1: | ||
== 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 [https://doi.org/10.1145/3694848.3694852]. 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. | I recently used Agda to check the type-correctness of a denotational semantics and the soundness of some proofs about it [https://doi.org/10.1145/3694848.3694852]. 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. | ||
Revision as of 15:18, 22 November 2024
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.
