Print Email Facebook Twitter Don’t bind yourself to do notation! Title Don’t bind yourself to do notation!: Using Agda to Prove Correctness of Refactorings on Monads Author Zandbergen, Timen (TU Delft Electrical Engineering, Mathematics and Computer Science) Contributor Miljak, L. (mentor) Cockx, J.G.H. (mentor) Langendoen, K.G. (graduation committee) Degree granting institution Delft University of Technology Programme Computer Science and Engineering Project CSE3000 Research Project Date 2023-06-30 Abstract This paper provides a refactoring from do notation to >>= operators and proves that this refactoring maintains observational equivalence. As programs grow ever larger and more complex, there is a growing need to automatically apply refactorings to these programs in a dependable manner. Current refactoring engines often contain errors, even if they are widely used and thoroughly tested. The methods used in the proof of contextual equivalence are described in this paper, with the goal of supporting future research into correct-by-construction refactorings. Subject correct-by-constructionrefactoringagda To reference this document use: http://resolver.tudelft.nl/uuid:e4c7d17f-b4c7-48ac-b1e6-834d82c26dc3 Part of collection Student theses Document type bachelor thesis Rights © 2023 Timen Zandbergen Files PDF main.pdf 188.26 KB Close viewer /islandora/object/uuid:e4c7d17f-b4c7-48ac-b1e6-834d82c26dc3/datastream/OBJ/view