Correct-by-construction refactoring of functional code

This repository contains a correct-by-construction approach for refactoring tuples to records in a Haskell-like language (HLL). This is done for the 2022/2023 edition of the BSc Research Project at the Delft Univesity of Technology. An example of the refactoring operation is shown below.

-- Before
lastName :: (String, String, Int) -> String
lastName (_, s, _) = s

-- After
data Person = Person { initials :: String
                     , lastName :: String
                     , age :: Int
                     }

---

Folder structure

All relevant information can be found in the src folder. The structure is as follows:

• HLL - Intrinsically-typed specification of the HLL and big-step semantics.
• Proofs - Proof that the refactoring operation replaces all tuples by record instances and a relation between values of a pre-refactored and refactored expression.
• Refactoring - Refactoring operation that replaces all tuples by record instances. Treats all tuples as if they were unique. The accompanying record declaration is based on the type signature of the tuple.
• Utils - Utility folder that contains a construct which specifies that some element is in a list.