Remember Me
Or use your Academic/Social account:


Or use your Academic/Social account:


You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.


Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message


Verify Password:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Sultana, Nik; Thompson, Simon (2008)
Languages: English
Types: Unknown
Subjects: QA76

Classified by OpenAIRE into

The paper surveys how software tools such as refactoring systems can be validated, and introduces a new mechanism, namely the extraction of a refactoring engine for a functional programming language from an Isabelle/HOL theory in which it is verified. This research is a first step in a programme to construct certified programming tools from verified theories. We also provide some empirical evidence of how refactoring can be of significant benefit in reshaping automatically-generated program code for use in larger systems.
  • The results below are discovered through our pilot algorithms. Let us know how we are doing!

    • [1] H. Barendregt. The Lambda Calculus, its Syntax and Semantics. North-Holland, 1984.
    • [2] S. Blazy, Z. Dargaye, and X. Leroy. Formal Verification of a C Compiler Front-end. Symp. on Formal Methods, pages 460-475, 2006.
    • [3] M. CorneĀ“lio. Refactorings as Formal Refinements. PhD thesis, Universidade Federal de Pernambuco, 2004.
    • [4] B. Daniel, D. Dig, K. Garcia, and D. Marinov. Automated testing of refactoring engines. In Proceedings of Foundations of Software Engineering (FSE'07), Dubrovnik, Croatia, Sep 2007.
    • [5] K. Elphinstone, G. Klein, and R. Kolanski. Formalising a high-performance microkernel. In R. Leino, editor, Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 06), Microsoft Research Technical Report MSR-TR-2006-117, pages 1-7, Seattle, USA, Aug. 2006.
    • [6] R. Ettinger. Refactoring via Program Slicing and Sliding. PhD thesis, Oxford University Computing Laboratory, June 2007.
    • [7] M. Fowler and K. Beck. Refactoring: Improving the Design of Existing Code. Addison-Wesley Professional, 1999.
    • [8] A. Garrido and J. Meseguer. Formal Specification and Verification of Java Refactorings. Proceedings of the Sixth IEEE International Workshop on Source Code Analysis and Manipulation (SCAM'06)-Volume 00, pages 165-174, 2006.
    • [9] W. Griswold. Program Restructuring as an Aid to Software Maintenance. PhD thesis, University of Washington, 1991.
    • [10] F. Haftmann and T. Nipkow. A code generator framework for Isabelle/HOL. Technical Report 364/07, Department of Computer Science, University of Kaiserslautern, 08 2007.
    • [11] A. Junior, L. Silva, and M. CorneĀ“lio. Using CafeOBJ to Mechanise Refactoring Proofs and Application. Electronic Notes in Theoretical Computer Science, 184:39- 61, 2007.
    • [12] X. Leroy. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. ACM SIGPLAN Notices, 41(1):42-54, 2006.
    • [13] H. Li. Refactoring Haskell Programs. PhD thesis, Computing Laboratory, University of Kent, September 2006.
    • [14] H. Li and S. Thompson. Formalisation of Haskell Refactorings. In M. van Eekelen and K. Hammond, editors, Trends in Functional Programming, September 2005.
    • [15] H. Li and S. Thompson. Testing Erlang Refactorings with QuickCheck. In Draft Proceedings of the 19th International Symposium on Implementation and Application of Functional Languages, IFL 2007, Freiburg, Germany, Sep 2007.
    • [16] T. Mossakowski, C. Maeder, and K. Luttich. The Heterogeneous Tool Set, HETS. LECTURE NOTES IN COMPUTER SCIENCE, 4424:519, 2007.
    • [17] T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002.
    • [18] K. Okuma and Y. Minamide. Executing Verified Compiler Specification. Programming Languages and Systems: First Asian Symposium, APLAS 2003, Beijing, China, November 27-29, 2003: Proceedings, 2003.
    • [19] L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer, 1994.
    • [20] B. Pierce. Types and Programming Languages. MIT Press, 2002.
    • [21] G. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5(3):223-255, 1977.
    • [22] N. Sultana and S. Thompson. Mechanical Verification of Refactorings. In Workshop on Partial Evaluation and Program Manipulation. ACM SIGPLAN, January 2008.
    • [23] S. Thompson. Formulating Haskell. Technical Report 29-92*, University of Kent, Computing Laboratory, University of Kent, Canterbury, UK, November 1992.
    • [24] S. Thompson. A Logic for Miranda, Revisited. Formal Aspects of Computing, 7(7), March 1995.
    • [25] P. Torrini, C. Lueth, C. Maeder, and T. Mossakowski. Translating haskell to isabelle. Number 364/07, 08 2007.
  • No related research data.
  • No similar publications.

Share - Bookmark

Download from

Cite this article