Polar: A Framework for Proof Refactoring

Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8312)


We present a prototype refactoring framework based on graph rewriting and bidirectional transformations that is designed to be generic, extensible, and declarative. Our approach uses a language-independent graph meta-model to represent proof developments in a generic way. We use graph rewriting to enrich the meta-model with dependency information and to perform refactorings, which are written as declarative rewrite rules. Our framework, called Polar, is implemented in the GrGen rewriting engine.


Type Graph Abstract Syntax Tree Bidirectional Transformation Abstraction Function Interactive Theorem Prove 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Arias, T.B.C., van der Spek, P., Avgeriou, P.: A practice-driven systematic review of dependency analysis solutions. Empirical Software Engineering 16(5), 544–586 (2011)CrossRefGoogle Scholar
  2. 2.
    Aschbacher, M.: Highly complex proofs and implications of such proofs. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences 363, 2401–2406 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Autexier, S., Dietrich, D., Hutter, D., Lüth, C., Maeder, C.: Smartties - management of safety-critical developments. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol. 7609, pp. 238–252. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  4. 4.
    Bancilhon, F., Spyratos, N.: Update semantics of relational views. ACM Trans. Database Syst. 6(4), 557–575 (1981)CrossRefGoogle Scholar
  5. 5.
    Bell Canada. DATRIX abstract semantic graph reference manual (version 1.4). Technical report (2000)Google Scholar
  6. 6.
    Bourke, T., Daum, M., Klein, G., Kolanski, R.: Challenges and experiences in managing large-scale proofs. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS (LNAI), vol. 7362, pp. 32–48. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  7. 7.
    Chen, H., Liao, H.: A comparative study of view update problem. In: Data Storage and Data Engineering (DSDE), pp. 83–89 (2010)Google Scholar
  8. 8.
    de Lara, J., Bardohl, R., Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Attributed graph transformation with node type inheritance. Theor. Comput. Sci. 376(3), 139–163 (2007)CrossRefzbMATHGoogle Scholar
  9. 9.
    Dietrich, D.: Assertion Level Proof Planning with Compiled Strategies. PhD thesis, Saarland University (2011)Google Scholar
  10. 10.
    Ferrante, J., Ottenstein, K.J., Warren, J.D.: The program dependence graph and its use in optimization. ACM Trans. Program. Lang. Syst. 9(3), 319–349 (1987)CrossRefzbMATHGoogle Scholar
  11. 11.
    Geiß, R., Batz, G.V., Grund, D., Hack, S., Szalkowski, A.: GrGen: A fast SPO-based graph rewriting tool. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 383–397. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  12. 12.
    Gonthier, G.: The Four Colour Theorem: Engineering of a formal proof. In: Kapur, D. (ed.) ASCM 2007. LNCS (LNAI), vol. 5081, p. 333. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  13. 13.
    Gonthier, G., et al.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 163–179. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  14. 14.
    Gonthier, G., Mahboubi, A., Rideau, L., Tassi, E., Théry, L.: A Modular Formalisation of Finite Group Theory. Rapport de recherche RR-6156, INRIA (2007)Google Scholar
  15. 15.
    Gordon, M., Milner, R., Morris, L., Newey, M., Wadsworth, C.: A metalanguage for interactive proof in LCF. In: Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1978, pp. 119–130. ACM, New York (1978)Google Scholar
  16. 16.
    Hales, T.C.: Introduction to the Flyspeck project. In: Coquand, T., Lombardi, H., Roy, M.-F. (eds.) Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, vol. 05021 (2006)Google Scholar
  17. 17.
    Hofmann, M., Pierce, B., Wagner, D.: Edit lenses. In: ACM SIGPLAN Notices, vol. 47, pp. 495–508. ACM (2012)Google Scholar
  18. 18.
    Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., et al.: seL4: Formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, pp. 207–220. ACM (2009)Google Scholar
  19. 19.
    Mens, T., Eetvelde, N.V., Demeyer, S., Janssens, D.: Formalizing refactorings with graph transformations. Journal of Software Maintenance 17(4), 247–276 (2005)CrossRefGoogle Scholar
  20. 20.
    Opdyke, W.F.: Refactoring object-oriented frameworks. PhD thesis, Champaign, IL, USA (1992)Google Scholar
  21. 21.
    Stevens, P.: A landscape of bidirectional model transformations. In: Lämmel, R., Visser, J., Saraiva, J. (eds.) GTTSE 2007. LNCS, vol. 5235, pp. 408–424. Springer, Heidelberg (2008)Google Scholar
  22. 22.
    Verbaere, M., Ettinger, R., de Moor, O.: JunGL: a scripting language for refactoring. In: Rombach, D., Soffa, M.L. (eds.) ICSE 2006: Proceedings of the 28th International Conference on Software Engineering, pp. 172–181. ACM Press, New York (2006)Google Scholar
  23. 23.
    Wenzel, M.T.: 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)CrossRefGoogle Scholar
  24. 24.
    Whiteside, I.: Refactoring Proofs. PhD thesis, University of Edinburgh (2013)Google Scholar
  25. 25.
    Whiteside, I., Aspinall, D., Dixon, L., Grov, G.: Towards formal proof script refactoring. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Calculemus/MKM 2011. LNCS (LNAI), vol. 6824, pp. 260–275. Springer, Heidelberg (2011)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  1. 1.Cyber-Physical Systems, DFKI BremenGermany
  2. 2.School of Computing ScienceNewcastle UniversityUK
  3. 3.School of InformaticsThe University of EdinburghUK

Personalised recommendations