Formally proving the correctness of the (un)currying refactoring

Using Agda with a simple Haskell-like programming language

Bachelor thesis (2023)

Authors

M.G. Jóźwik 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 Michał Jóźwik
Agda Correct by construction Haskell Formal Verification Refactoring
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

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.