Monae: Monadic Effects and Equational Reasoning in Coq
Functional programs with side effects represented by monads are amenable to equational reasoning. This approach to program verification is called monadic equational reasoning and has been experimented several times using proof assistants based on dependent type theory. In order to improve such formalizations, we study Monae, a Coq library that supports monadic equational reasoning.
Our member, Ayumu Saito, is participating in the Monae project under the supervision by Reynald Affeldt at AIST.
News
- Poster Presentations at PPL 2024
- Saito, Tsunoda and Tsuyama presented Master’s Thesis
- APLAS 2023 Paper on a Mechanized Formalization of a Probabilistic Programming Language
- 3 Talks on formalization at TPP 2023
- TyDe 2023 Talk on a Probabilistic Programming Language
- Poster Presentations at PPL 2023
- Paper presentation on Monadic Equational Reasoning at MPC 2022
- PPL2022 Paper on Monadic Equational Reasoning (along with other paper and poster presentations)
- Saito, Tsunoda and Tsuyama Presented Bachelor’s Theses
- Talk on Monadic Equation Reasoning (@ TPP2021)