Skip to content

Research at St Andrews

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Author(s)

School/Research organisations

Abstract

We present a formally verified refactoring framework for a subset of Haskell 98. Our framework 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.
Close

Details

Original languageEnglish
Title of host publication8th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2021)
Pages1-10
Number of pages10
Publication statusPublished - 18 Jul 2021
Event8th 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

Workshop8th International Workshop on Rewriting Techniques for Program Transformations and Evaluation
Abbreviated titleWPTE 2021
Country/TerritoryArgentina
CityBuenos Aeires
Period18/07/21 → …
Internet address

    Research areas

  • Haskell, Refactoring, Dependent types, Idris, Renaming, Proof-carrying code, Soundness

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Timing properties and correctness for structured parallel programs on x86-64 multicores

    Hammond, K., Brown, C. M. & Sarkar, S., 2016, Foundational and Practical Aspects of Resource Analysis: 4th International Workshop, FOPARA 2015, London, UK, April 11, 2015. Revised Selected Papers. van Eekelen, M. & Dal Lago, U. (eds.). Springer, p. 101-125 26 p. (Lecture Notes in Computer Science; vol. 9964).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  2. Restoration of legacy parallelism: transforming pthreads into farm and pipeline patterns

    Janjic, V., Brown, C. M. & Barwell, A., 11 Jun 2021, In: International Journal of Parallel Programming. First Online, 25 p.

    Research output: Contribution to journalArticlepeer-review

  3. Fast and correct load-link/store-conditional instruction handling in DBT systems

    Kristien, M., Spink, T., Campbell, B., Sarkar, S., Stark, I., Franke, B., Böhm, I. & Topham, N., 2 Oct 2020, CASES '20: Proceedings of the International Conference on Compilers, Architectures and Synthesis for Embedded Systems. IEEE Computer Society, Vol. Early Access. 11 p. (IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  4. Programming heterogeneous parallel machines using refactoring and Monte-Carlo tree search

    Brown, C. M., Janjic, V., Goli, M. & McCall, J., Aug 2020, In: International Journal of Parallel Programming. 48, 4, p. 583–602 20 p.

    Research output: Contribution to journalArticlepeer-review

  5. Refactoring GrPPI: generic refactoring for generic parallelism in C++

    Brown, C. M., Janjic, V., Barwell, A. D., Garcia, J. D. & MacKenzie, K., 10 Jul 2020, (E-pub ahead of print) In: International Journal of Parallel Programming. First Online, 23 p.

    Research output: Contribution to journalArticlepeer-review

ID: 275239759

Top