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

Contact

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
Archive of Formal Proofs 2014.

Certification Monads
Christian Sternagel and René Thiemann
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
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.