Formalizing Open Induction, The Tree Theorem, and Simple Termination


Proving termination is an important part of program verification. To facilitate reusable and abstract results, instead of a concrete programming language, termination is usually considered relative to a mathematical model of computation, for this project, term rewriting. Nowadays, there are many tools that can prove termination of term rewriting automatically. However, these tools may contain bugs and hence the need for an independent and reliable certification of their results arises. This is done by so called certifiers, tools that can automatically check, whether a proof that was generated by a termination tool, is correct. The high reliability of such certifiers comes from the fact that they are built upon formalizations of the underlying theory using proof assistants, like Isabelle/HOL. One such formalization is IsaFoR, an Isabelle Formalization of Rewriting. Naturally, formalizations in Isabelle can only build upon facts that have already been formalized in Isabelle before. Hence, one aim of this project is to widen the body of mathematics that is available to Isabelle users. The concrete new contributions will be a formalization of (possibly infinite) trees and upon that a proof of the famous Tree Theorem by Kruskal in Isabelle. The Tree Theorem, in turn, will allow to formalize the connection between simple termination and termination: every simply terminating term rewrite system is also terminating. This result will then be used to incorporate the Knuth-Bendix order (and possibly other simplification orders) into IsaFoR, thereby increasing the number of termination proofs that can be certified automatically. However, we are not only interested in the Tree Theorem with respect to simple termination, but also in its computational content. To this end, we will formalize the principle of open induction in Isabelle, in order to be able to give an alternative and more constructive proof of the Tree Theorem. Furthermore, we will search for other theorems, where open induction could facilitate a formalized proof. Finally, open induction can also be used to define total functions. Since proof assistants based on higher-order logic (as Isabelle) rely on all defined functions being total, we will use open induction to extend Isabelle’s definitional function package by open inductively defined functions.

project start: November 2011
project end: November 2014

 Members
  • Christian Sternagel
FWF Erwin Schrödinger Fellowship Abroad project number

J3202

  Contact

christian.sternagel@uibk.ac.at

Publications
  • A Framework for Developing Stand-Alone Certifiers
    Christian Sternagel and René Thiemann
    Proceedings of the 9th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2014), Electronic Notes in Theoretical Computer Science 312, pp. 51 – 67, 2015.
  • XML
    Christian Sternagel and René Thiemann
    The Archive of Formal Proofs, 2014.
  • Certification Monads
    Christian Sternagel and René Thiemann
    The Archive of Formal Proofs, 2014.
  • The Certification Problem Format
    Christian Sternagel and René Thiemann
    Proceedings of the 11th International Workshop on User Interfaces for Theorem Provers (UITP 2014), Electronic Proceedings in Theoretical Computer Science 167, pp. 61 – 72, 2014.
  • Haskell’s Show-Class in Isabelle/HOL
    Christian Sternagel and René Thiemann
    The Archive of Formal Proofs, 2014.
  • A New and Formalized Proof of Abstract Completion
    Nao Hirokawa, Aart Middeldorp, and Christian Sternagel
    Proceedings of the 5th International Conference on Interactive Theorem Proving (ITP 2014), Lecture Notes in Computer Science 8558, pp. 292 – 307, 2014.
  • Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs
    Christian Sternagel and René Thiemann
    Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014), Lecture Notes in Computer Science 8560, pp. 441 – 455, 2014.
  • Normalization Equivalence of Rewrite Systems
    Nao Hirokawa, Aart Middeldorp, and Christian Sternagel
    Proceedings of the 3rd International Workshop on Confluence (IWC 2014),   pp. 14 – 18, 2014.
  • Certified Kruskal’s Tree Theorem
    Christian Sternagel
    Journal of Formalized Reasoning 7(1), pp. 45 – 62, 2014.
  • Certified Kruskal's Tree Theorem
    Christian Sternagel
    Proceedings of the 3rd International Conference on Certified Programs and Proofs (CPP 2013), Lecture Notes in Computer Science 8307, pp. 178 – 193, 2013.
  • A Haskell Library for Term Rewriting
    Bertram Felgenhauer, Martin Avanzini, and Christian Sternagel
    Proceedings of the 1st International Workshop on Haskell and Rewriting Techniques (HART 2013),  2013
  • Certified HLints with Isabelle/HOLCF-Prelude
    Joachim Breitner, Brian Huffman, Neil Mitchell, and Christian Sternagel
    Proceedings of the 1st International Workshop on Haskell and Rewriting Techniques (HART 2013),  2013.
  • Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion
    Christian Sternagel and René Thiemann
    Proceedings of the 24th International Conference on Rewriting Techniques and Applications (RTA 2013), Leibniz International Proceedings in Informatics 21, pp. 287 – 302, 2013.
  • Open Induction
    Mizuhito Ogawa and Christian Sternagel
    The Archive of Formal Proofs, 2012.
  • Proof Pearl - A Mechanized Proof of GHC's Mergesort
    Christian Sternagel
    Journal of Automated Reasoning 51(4), pp. 357 – 370, 2012.
  • A Locale for Minimal Bad Sequences
    Christian Sternagel
    Isabelle Users Workshop (IUW 2012),  2012.
  • Getting Started with Isabelle/jEdit
    Christian Sternagel
    Isabelle Users Workshop (IUW 2012),  2012.
  • Well-Quasi-Orders
    Christian Sternagel
    The Archive of Formal Proofs, 2012.
  • Certification of Nontermination Proofs
    Christian Sternagel and René Thiemann
    Proceedings of the 3rd International Conference on Interactive Theorem Proving (ITP 2012), Lecture Notes in Computer Science 7406, pp. 266 – 282, 2012.
  • Recording Completion for Finding and Certifying Proofs in Equational Logic
    Thomas Sternagel, René Thiemann, Harald Zankl, and Christian Sternagel
    Proceedings of the 1st International Workshop on Confluence (IWC 2012),   pp. 31 – 36, 2012.
  • A Relative Dependency Pair Framework
    Christian Sternagel and René Thiemann
    Proceedings of the 13th International Workshop on Termination (WST 2012),   pp. 79 – 83, 2012.
Nach oben scrollen