Formally proving the correctness of the (un)currying refactoring
Using Agda with a simple Haskell-like programming language
M.G. Jóźwik (TU Delft - Electrical Engineering, Mathematics and Computer Science)
J.G.H. Cockx – Mentor (TU Delft - Programming Languages)
L. Miljak – Mentor (TU Delft - Programming Languages)
Koen Langendoen – Graduation committee member (TU Delft - Embedded Systems)
More Info
expand_more
Repository containing the code created for the project
https://github.com/MetaBorgCube/brp-agda-refactoring-mjozwikOther 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.
Abstract
When designing critical software, great care must be taken to guarantee its correctness. Refactoring is one of the techniques used to improve code readability, maintainability, and other factors without changing functionality. Thus, to ensure that it is properly applied, automated tools are used to perform refactoring. To ensure that the code remained correct, we verified the correctness of the tool actions using formal proof. This is assisted by a dependently typed language Agda, which, when used as a proof assistant, can directly support us by ensuring the soundness of the steps taken. We consider the refactoring of currying and its counterpart, uncurrying, using a small proof-of-concept functional programming language with intrinsically typed terms and de Bruijn indices. Furthermore, we proved the retained properties of well-typedness, termination, and value relation of the input program. Finally, we argue that this research could be extended to the full implementation of Haskell, as well as applied to other languages and similar refactorings.