Maybe a List would be better?
Correct by construction Maybe to List refactorings in a Haskell-like language
J.C. Padilla Cancio (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Jesper 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
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.
Abstract
This paper concerns itself with correct by construction refactoring of Maybe values to List values in a Haskell-like language (HLL) as a case study on data-oriented refactorings. Our language makes use of intrinsically-typed syntax and de Bruijn indices for variables. Operational semantics are defined using big step semantics. We define a refactoring function which intrinsically verifies its well-typedness due to our intrinsically-typed syntax. The semantic validity of this refactoring is given by a separate proof. We use Agda, a functional language and theorem prover, to define and prove these properties. Techniques and concepts used in our refactoring and proof generalize well to other data-oriented refactorings.