Difference between revisions of "WG211/M24Mosses"
From WG 2.11
(Initial version.) |
(Add link to a paper.) |
||
| (One intermediate revision by the same user not shown) | |||
| Line 1: | Line 1: | ||
| − | 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. | + | |
| + | == 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 [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. | ||
Latest revision as of 15:39, 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 (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.
