Proving correctness of refactoring tuples to records

Proving correctness of refactoring tuples to records: A correct-by-construction approach on a Haskell-like language

Bastenhof, Jeroen (TU Delft Electrical Engineering, Mathematics and Computer Science; TU Delft Programming Languages)

Cockx, J.G.H. (mentor)
Miljak, L. (mentor)
Langendoen, K.G. (graduation committee)

Delft University of Technology

Computer Science and Engineering

CSE3000 Research Project

2023-06-30

Refactoring is a useful tool for increasing the overall quality of software without making changes to how it interacts with the environment. To verify that a refactoring operation correctly transforms an expression, one can provide a formal proof. Using Agda, a dependently-typed language, as a proof assistant, we investigate the feasibility of proving the correctness of refactoring tuples to records for a small-scale language that shares similarities with Haskell. We construct this language in Agda using intrinsically-typed terms and define an accompanying refactoring function for refactoring tuples to records. We prove that the refactoring is well-typed and that it replaces all tuple occurrences. Big-step semantics are used to show the relation between the intrinsically-typed language and its resulting output value. Additionally, we show that we can construct a relation between the values of an expression before and after refactoring. By presenting these proofs we gain more insights into the feasibility of proving the correctness of tuple to record refactoring. Furthermore, we argue that the proofs given for this small-scale language can serve as inspiration for proving comparable properties of the refactoring in the context of Haskell and beyond.

Agda
Refactoring
Dependent Types
Haskell

http://resolver.tudelft.nl/uuid:e61b0972-175e-42d3-bb10-d7ee9f2584ea

https://github.com/JerBast/brp-agda-refactoring-jbastenhof

Student theses

bachelor thesis

© 2023 Jeroen Bastenhof