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

Adam David Barwell; Christopher Mark Brown; Susmit Sarkar

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

Adam David Barwell, Christopher Mark Brown, Susmit Sarkar

School of Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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 us to encode soundness proofs as an integral part of the implementation. We give the formal definition of our static semantics for our Haskell 98 subset, which we encode as part of the AST, ensuring that only well-formed programs may be represented and transformed. This forms a foundation upon which refactorings can be formally specified. We then define soundness of refactoring implementations as conformity to their specification. We demonstrate our approach via renaming, a canonical and well-understood refactoring, giving its implementation alongside its formal specification and soundness proof.

Original language	English
Title of host publication	8^th International workshop on rewriting techniques for program transformations and evaluation (WPTE 2021)
Number of pages	10
Publication status	Published - 18 Jul 2021
Event	8th International Workshop on Rewriting Techniques for Program Transformations and Evaluation - Argentina, Buenos Aeires, Argentina Duration: 18 Jul 2021 → … Conference number: 8 https://www.ipl.riec.tohoku.ac.jp/wpte2021/

Workshop

Workshop	8th International Workshop on Rewriting Techniques for Program Transformations and Evaluation
Abbreviated title	WPTE 2021
Country/Territory	Argentina
City	Buenos Aeires
Period	18/07/21 → …
Internet address	https://www.ipl.riec.tohoku.ac.jp/wpte2021/

Keywords

Haskell
Refactoring
Dependent types
Idris
Renaming
Proof-carrying code
Soundness

Access to Document

WPTE2021
Copyright 2021 © A. Barwell, C. Brown & S. Sarkar. This work is licensed under the Creative Commons Attribution License.
Accepted author manuscript, 214 KBLicence: CC BY

Cite this

@inproceedings{8d71d5b324724fdeafda55c21286ccf2,

title = "Proving renaming for Haskell via dependent types: a case-study in refactoring soundness",

abstract = "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 us to encode soundness proofs as an integral part of the implementation. We give the formal definition of our static semantics for our Haskell 98 subset, which we encode as part of the AST, ensuring that only well-formed programs may be represented and transformed. This forms a foundation upon which refactorings can be formally specified. We then define soundness of refactoring implementations as conformity to their specification. We demonstrate our approach via renaming, a canonical and well-understood refactoring, giving its implementation alongside its formal specification and soundness proof.",

keywords = "Haskell, Refactoring, Dependent types, Idris, Renaming, Proof-carrying code, Soundness",

author = "Barwell, {Adam David} and Brown, {Christopher Mark} and Susmit Sarkar",

year = "2021",

month = jul,

day = "18",

language = "English",

booktitle = "8th International workshop on rewriting techniques for program transformations and evaluation (WPTE 2021)",

note = "8th International Workshop on Rewriting Techniques for Program Transformations and Evaluation<br/>, WPTE 2021 ; Conference date: 18-07-2021",

url = "https://www.ipl.riec.tohoku.ac.jp/wpte2021/",

}

Barwell, AD , Brown, CM & Sarkar, S 2021, Proving renaming for Haskell via dependent types: a case-study in refactoring soundness. in 8^th International workshop on rewriting techniques for program transformations and evaluation (WPTE 2021). 8th International Workshop on Rewriting Techniques for Program Transformations and Evaluation
, Buenos Aeires, Argentina, 18/07/21.

TY - GEN

T1 - Proving renaming for Haskell via dependent types

T2 - 8th International Workshop on Rewriting Techniques for Program Transformations and Evaluation<br/>

AU - Barwell, Adam David

AU - Brown, Christopher Mark

AU - Sarkar, Susmit

N1 - Conference code: 8

PY - 2021/7/18

Y1 - 2021/7/18

N2 - 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 us to encode soundness proofs as an integral part of the implementation. We give the formal definition of our static semantics for our Haskell 98 subset, which we encode as part of the AST, ensuring that only well-formed programs may be represented and transformed. This forms a foundation upon which refactorings can be formally specified. We then define soundness of refactoring implementations as conformity to their specification. We demonstrate our approach via renaming, a canonical and well-understood refactoring, giving its implementation alongside its formal specification and soundness proof.

AB - 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 us to encode soundness proofs as an integral part of the implementation. We give the formal definition of our static semantics for our Haskell 98 subset, which we encode as part of the AST, ensuring that only well-formed programs may be represented and transformed. This forms a foundation upon which refactorings can be formally specified. We then define soundness of refactoring implementations as conformity to their specification. We demonstrate our approach via renaming, a canonical and well-understood refactoring, giving its implementation alongside its formal specification and soundness proof.

KW - Haskell

KW - Refactoring

KW - Dependent types

KW - Idris

KW - Renaming

KW - Proof-carrying code

KW - Soundness

UR - https://www.ipl.riec.tohoku.ac.jp/wpte2021/

UR - https://www.sciencedirect.com/journal/journal-of-logical-and-algebraic-methods-in-programming/special-issues

UR - https://fscd2021.dc.uba.ar/

M3 - Conference contribution

BT - 8th International workshop on rewriting techniques for program transformations and evaluation (WPTE 2021)

Y2 - 18 July 2021

ER -

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

Abstract

Workshop

Keywords

Access to Document

Other files and links

Fingerprint

Energise: Refactorings and Skeletons for: Energise: Refactorings and Skeletons for Energy-Aware Applications on High-Performance Embedded Systems

TeamPlay: H2020 ICT-5 Teamplay

Discovery: Pattern Discovery and Program: Discovery: Pattern Discovery and Program Shaping for Manycore Systems

Cite this

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

Abstract

Workshop

Keywords

Access to Document

Other files and links

Fingerprint

Projects

Energise: Refactorings and Skeletons for: Energise: Refactorings and Skeletons for Energy-Aware Applications on High-Performance Embedded Systems

TeamPlay: H2020 ICT-5 Teamplay

Discovery: Pattern Discovery and Program: Discovery: Pattern Discovery and Program Shaping for Manycore Systems

Cite this