Christopher Brown

Proving renaming for Haskell via dependent types : a case-study in refactoring soundness

2021 · St Andrews Research Repository (St Andrews Research Repository)

We present a formally verified renaming refactoring for a subset of Haskell 98 giving a case-study in proving soundness properties of Haskell refactorings. Our renaming is implemented in the dependently- typed language Idris, which allows …