Nita, Andrei-Alexandru (2025) Programming and Reasoning with Monads. Bachelor's Thesis, Computing Science.
|
Text
bCS2025NitaAA.pdf Download (268kB) | Preview |
|
![[img]](https://fse.studenttheses.ub.rug.nl/style/images/fileicons/text.png) |
Text
Toestemming.pdf Restricted to Registered users only Download (154kB) |
Abstract
Monads provide a structured way to model side effects in functional programming. In the Rocq proof assistant, monads make it possible to represent and reason about computations involving effects such as state, exceptions, or input/output. While monads are commonly used in programming, their use in formal verification raises challenges, such as combining multiple effects or scaling up proofs. This thesis presents a systematic implementation and comparison of several monads in Rocq, including State, Exception, Reader, Writer, Maybe, and Identity. For each monad, we define its structure, prove the monad laws, and build verified examples. We then generalize the approach using type classes for monads and their laws, and we extend the system with the StateT monad transformer. By analyzing how different monads behave in practice, we examine how they support structured effect handling, what challenges they introduce in proofs and reasoning, and how they scale in Rocq. The goal is to connect monadic theory with practical use in formal verification and to to understand how different monads affect reasoning complexity and proof structure.
| Item Type: | Thesis (Bachelor's Thesis) |
|---|---|
| Supervisor name: | Frumin, D. and Perez Parra, J.A. |
| Degree programme: | Computing Science |
| Thesis type: | Bachelor's Thesis |
| Language: | English |
| Date Deposited: | 31 Jul 2025 08:56 |
| Last Modified: | 31 Jul 2025 08:56 |
| URI: | https://fse.studenttheses.ub.rug.nl/id/eprint/36614 |
Actions (login required)
 |
View Item |