Abstract
Expressive logics, such as the modal μ-calculus, can be used to specify and verify functional requirements of program models. While such verification is useful, a key challenge is to guarantee that the model being verified actually corresponds to the (typically effectful) program it is supposed to. We explore an approach that bridges this gap between effectful programming and functional requirement verification. Using dependently-typed programming in Agda, we develop an embedding of the modal μ-calculus for defining and verifying functional properties of possibly-non-terminating effectful programs which we represent in Agda using the coinductive free monad.
| Original language | English |
|---|---|
| Title of host publication | TyDe 2024 |
| Subtitle of host publication | Proceedings of the 9th ACM SIGPLAN International Workshop on Type-Driven Development |
| Editors | Sandra Alves, Jesper Cockx |
| Place of Publication | New York, NY |
| Publisher | Association for Computing Machinery (ACM) |
| Pages | 16-28 |
| Number of pages | 13 |
| ISBN (Electronic) | 979-8-4007-1103-9 |
| DOIs | |
| Publication status | Published - 2024 |
| Event | 9th ACM SIGPLAN International Workshop on Type-Driven Development - Milano Convention Centre, Milan, Italy Duration: 6 Sept 2024 → 6 Sept 2024 https://icfp24.sigplan.org/home/tyde-2024 |
Workshop
| Workshop | 9th ACM SIGPLAN International Workshop on Type-Driven Development |
|---|---|
| Abbreviated title | TyDe 2024 |
| Country/Territory | Italy |
| City | Milan |
| Period | 6/09/24 → 6/09/24 |
| Internet address |
Keywords
- Agda
- Algebraic Effects
- Formal Verification
- Free Monad
- Modal μ-Calculus