Print Email Facebook Twitter Maybe a List would be better? Title Maybe a List would be better?: Correct by construction Maybe to List refactorings in a Haskell-like language Author Padilla Cancio, José (TU Delft Electrical Engineering, Mathematics and Computer Science) Contributor Cockx, J.G.H. (mentor) Miljak, L. (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 concerns itself with correct by construction refactoring of Maybe values to List values in a Haskell-like language (HLL) as a case study on data-oriented refactorings. Our language makes use of intrinsically-typed syntax and de Bruijn indices for variables. Operational semantics are defined using big step semantics. We define a refactoring function which intrinsically verifies its well-typedness due to our intrinsically-typed syntax. The semantic validity of this refactoring is given by a separate proof. We use Agda, a functional language and theorem prover, to define and prove these properties. Techniques and concepts used in our refactoring and proof generalize well to other data-oriented refactorings. Subject Programming LanguagesFunctional ProgrammingFormal VerificationAgdaCorrect by constructionRefactoring To reference this document use: http://resolver.tudelft.nl/uuid:5eb7fd17-c187-440f-b700-ebd123cab533 Part of collection Student theses Document type bachelor thesis Rights © 2023 José Padilla Cancio Files PDF CSE3000_Final_Paper_9.pdf 253.93 KB Close viewer /islandora/object/uuid:5eb7fd17-c187-440f-b700-ebd123cab533/datastream/OBJ/view