Proving correctness of refactoring tuples to records

A correct-by-construction approach on a Haskell-like language

Bachelor thesis (2023)

Authors

J. Bastenhof Electrical Engineering, Mathematics and Computer Science

Contributors

J.G.H. Cockx Programming Languages - EEMCS (supervisor 1)
L. Miljak Programming Languages - EEMCS (supervisor 1)
K.G. Langendoen Embedded Systems - EEMCS (supervisor 2)
Faculty
Electrical Engineering, Mathematics and Computer Science
Copyright: © 2023 Jeroen Bastenhof
More Info
expand_more

Published Date

30-06-2023

Language

English

Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Faculty

Electrical Engineering, Mathematics and Computer Science

Abstract

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.