Skip to main content
SpringerLink
Log in

Towards Formal Proof Script Refactoring

  • Conference paper
Intelligent Computer Mathematics (CICM 2011)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 6824))

Included in the following conference series:

Abstract

We propose proof script refactorings as a robust tool for constructing, restructuring, and maintaining formal proof developments. We argue that a formal approach is vital, and illustrate by defining and proving correct a number of valuable refactorings in a simplified proof script and declarative proof language of our own design.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aspinall, D., Denney, E., Lüth, C.: Tactics for hierarchical proof. Mathematics in Computer Science 3, 309–330 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  2. Corbineau, P.: A declarative language for the Coq proof assistant. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES 2007. LNCS, vol. 4941, pp. 69–84. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  3. Cornlio, M., Cavalcanti, A., Sampaio, A.: Refactoring by transformation. Electronic Notes in Theoretical Computer Science 70(3), 311–330 (2002)

    Article  MATH  Google Scholar 

  4. Denney, E., Power, J., Tourlas, K.: Hiproofs: A hierarchical notion of proof tree. Electr. Notes Theor. Comput. Sci. 155, 341–359 (2006)

    Article  MATH  Google Scholar 

  5. Ettinger, R., Verbaere, M.: Refactoring bugs in Eclipse, IntelliJ IDEA and Visual Studio (2005), http://progtools.comlab.ox.ac.uk/projects/refactoring/bugreports

  6. Fowler, M.: Refactoring: improving the design of existing code. Addison-Wesley, Reading (1999)

    MATH  Google Scholar 

  7. Gonthier, G.: The Four Colour Theorem: Engineering of a formal proof. In: Kapur, D. (ed.) ASCM 2007. LNCS (LNAI), vol. 5081, pp. 333–333. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  8. Hales, T.C.: Formal proof. Notices of the AMS 55, 1370–1380 (2008)

    MathSciNet  MATH  Google Scholar 

  9. Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: Proceedings of the 22nd ACM Symposium on OSP, pp. 207–220. ACM, New York (October 2009)

    Google Scholar 

  10. Li, H., Thompson, S.: Formalisation of Haskell Refactorings. In: Trends in Functional Programming (September 2005)

    Google Scholar 

  11. Mens, T., Tourwe, T.: A survey of software refactoring. IEEE Trans. Softw. Eng. 30(2), 126–139 (2004)

    Article  Google Scholar 

  12. Opdyke, W.F.: Refactoring object-oriented frameworks. PhD thesis, University of Illinois, Champaign, IL, USA (1992)

    Google Scholar 

  13. Pons, O., Bertot, Y., Rideau, L.: Notions of dependency in proof assistants. In: User Interfaces for Theorem Provers, UITP (1998)

    Google Scholar 

  14. Schairer, A., Hutter, D.: Proof transformations for evolutionary formal software development. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 441–456. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  15. Serjantov, A., Sewell, P., Wansbrough, K.: The UDP calculus: Rigorous semantics for real networking. In: Kobayashi, N., Babu, C. S. (eds.) TACS 2001. LNCS, vol. 2215, pp. 535–559. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  16. Stepney, S., Polack, F., Toyn, I.: Refactoring in maintenance and development of Z specifications. Electr. Notes Theor. Comput. Sci. 70(3) (2002)

    Google Scholar 

  17. Josef, U., Grzegorz, B.: Presenting and explaining Mizar. Electron. Notes Theor. Comput. Sci. 174(2), 63–74 (2007)

    Article  MATH  Google Scholar 

  18. Wenzel, M.: Isar - a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 167–184. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Informatics, University of Edinburgh, Edinburgh, EH8 9AB, Scotland

    Iain Whiteside, David Aspinall, Lucas Dixon & Gudmund Grov

Authors
  1. Iain Whiteside
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David Aspinall
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Lucas Dixon
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Gudmund Grov
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Departments of Computer Science and Mathematics Sciences, University of Bath, BA2 7AY, United Kingdom

    James H. Davenport

  2. Department of Computing and Software, McMaster University, 1280 Main Street West, L8SK1, Hamilton, Ontario, Canada

    William M. Farmer

  3. Institute for Computing and Information Sciences, Radboud University, Heyendaalseweg 135, 6525 AJ, Nijmegen, The Netherlands

    Josef Urban

  4. Department of Computer Science, Jacobs University Bremen, Campus Ring 12, 28759, Bremen, Germany

    Florian Rabe

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Whiteside, I., Aspinall, D., Dixon, L., Grov, G. (2011). Towards Formal Proof Script Refactoring. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds) Intelligent Computer Mathematics. CICM 2011. Lecture Notes in Computer Science(), vol 6824. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22673-1_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-22673-1_18

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-22672-4

  • Online ISBN: 978-3-642-22673-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation