Print Email Facebook Twitter Practical Verification of the Reader Monad Title Practical Verification of the Reader Monad Author Haršáni, Alex (TU Delft Electrical Engineering, Mathematics and Computer Science) Contributor Cockx, J.G.H. (mentor) Escot, L.F.B. (mentor) Wang, Qing (graduation committee) Degree granting institution Delft University of Technology Programme Computer Science and Engineering Project CSE3000 Research Project Date 2022-06-27 Abstract Agda2hs is a tool that allows developers to write verified programs using Agda and then translate these programs to Haskell while maintaining the verified properties. Previous research has shown that Agda2hs can be used to produce a verified implementation of a wide range of programs. However, monads that model effectful computations were largely unexplored in the context of Agda2hs. In this paper, we investigate the Reader monad, which gives us a way to model the global state. As monads are in practice commonly combined with other monads, we also investigate the transformer ReaderT. This paper provides the implementation of Reader and ReaderT in Agda, verifies its properties based on laws of type classes functor, applicative, and monad, as well as monad transformer laws for ReaderT, and assesses whether Agda2hs produces their correct and useful translation. Subject AgdaHaskellagda2hs To reference this document use: http://resolver.tudelft.nl/uuid:99a0e50b-c3a5-4a6b-8204-4815d96c68eb Part of collection Student theses Document type bachelor thesis Rights © 2022 Alex Haršáni Files PDF rp_final.pdf 146.09 KB Close viewer /islandora/object/uuid:99a0e50b-c3a5-4a6b-8204-4815d96c68eb/datastream/OBJ/view