Formally proving the correctness of the (un)currying refactoring

Formally proving the correctness of the (un)currying refactoring: Using Agda with a simple Haskell-like programming language

Jóźwik, Michał (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

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.

Agda
Formal Verification
Haskell
Refactoring
Correct by construction

http://resolver.tudelft.nl/uuid:7c4e74b3-d878-4d0a-acc2-541203d0874a

https://github.com/MetaBorgCube/brp-agda-refactoring-mjozwik Repository containing the code created for the project

Student theses

bachelor thesis

© 2023 Michał Jóźwik