Dr. Alexander Krauss

Preprints

• Ana Bove, Alexander Krauss, and Matthieu Sozeau. Partiality and recursion in interactive theorem provers: An overview. Revised version to appear in Mathematical Structures in Computer Science.

  The use of interactive theorem provers to establish the correctness of critical parts of a software development or for formalising mathematics is becoming more common and feasible in practice. However, most mature theorem provers lack a direct treatment of partial and general recursive functions; overcoming this weakness has been the objective of intensive research during the last decades. In this article, we review many techniques that have been proposed in the literature to simplify the formalisation of partial and general recursive functions in interactive theorem provers. Moreover, we classify the techniques according to their theoretical basis and their practical use. This uniform presentation of the different techniques facilitates the comparison and highlights their commonalities and differences, as well as their relative advantages and limitations. We focus on theorem provers based on constructive type theory (in particular, Agda and Coq) and higher-order logic (in particular Isabelle/HOL). Other systems and logics are covered to a certain extend, but not exhaustively. In addition to the description of the techniques, we also demonstrate tools which facilitate working with the problematic functions in particular theorem provers.

Refereed

• Alexander Krauss, Christian Sternagel, René Thiemann, Carsten Fuhs, and Jürgen Giesl. Termination of Isabelle functions via termination of rewriting. In Marko van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk, editors, Interactive Theorem Proving (ITP 2011), volume 6898 of Lecture Notes in Computer Science. Springer Verlag, 2011. (DOI)

  We show how to automate termination proofs for recursive functions in (a first-order subset of) Isabelle/HOL by encoding them as term rewrite systems and invoking an external termination prover. Our link to the external prover includes full proof reconstruction, where all necessary properties are derived inside Isabelle/HOL without oracles. Apart from the certification of the imported proof, the main challenge is the formal reduction of the proof obligation produced by Isabelle/HOL to the termination of the corresponding term rewrite system. We automate this reduction via suitable tactics which we added to the IsaFoR library.

• Jasmin Christian Blanchette and Alexander Krauss. Monotonicity inference for higher-order formulas. Journal of Automated Reasoning, 47(4), 2011. Extended version of the IJCAR 2010 paper. (DOI)

  Formulas are often monotonic in the sense that satisfiability for a given domain of discourse entails satisfiability for all larger domains. Monotonicity is undecidable in general, but we devised three calculi that infer it in many cases for higher-order logic. The third calculus has been implemented in Isabelle's model finder Nitpick, where it is used both to prune the search space and to soundly interpret infinite types with finite sets, leading to dramatic speed and precision improvements.

• Alexander Krauss and Tobias Nipkow. Proof pearl: Regular expression equivalence and relation algebra. Journal of Automated Reasoning, 2011. To appear. (DOI)

  We describe and verify an elegant equivalence checker for regular expressions. It works by constructing a bisimulation relation between (derivatives of) regular expressions. By mapping regular expressions to binary relations, an automatic and complete proof method for (in)equalities of binary relations over union, composition and (reflexive) transitive closure is obtained. The verification is carried out in the theorem prover Isabelle/HOL, yielding a practically useful decision procedure.

• Alexander Krauss. Recursive definitions of monadic functions. In Ana Bove, Ekaterina Komendantskaya, and Milad Niqui, editors, Workshop on Partiality and Recursion in Interactive Theorem Proving (PAR 2010), volume 43 of EPTCS, pages 1–13, 2010. (DOI)

  Using standard domain-theoretic fixed-points, we present an approach for defining recursive functions that are formulated in monadic style. The method works both in the simple option monad and the state-exception monad of Isabelle/HOL's imperative programming extension, which results in a convenient definition principle for imperative programs, which were previously hard to define. For such monadic functions, the recursion equation can always be derived without preconditions, even if the function is partial. The construction is easy to automate, and convenient induction principles can be derived automatically.

• Jasmin Christian Blanchette and Alexander Krauss. Monotonicity inference for higher-order formulas. In Jürgen Giesl and Reiner Hähnle, editors, Automated Reasoning (IJCAR 2010), volume 6173 of Lecture Notes in Artificial Intelligence, pages 91–106. Springer Verlag, 2010. (DOI)

  Formulas are often monotonic in the sense that if the formula is satisfiable for given domains of discourse, it is also satisfiable for all larger domains. Monotonicity is undecidable in general, but we devised two calculi that infer it in many cases for higher-order logic. The stronger calculus has been implemented in Isabelle's model finder Nitpick, where it is used to prune the search space, leading to dramatic speed improvements for formulas involving many atomic types.

• Alexander Krauss and Andreas Schropp. A mechanized translation from higher-order logic to set theory. In Matt Kaufmann and Lawrence C. Paulson, editors, Interactive Theorem Proving (ITP 2010), volume 6172 of Lecture Notes in Computer Science, pages 323–338. Springer Verlag, 2010. (DOI)

  In order to make existing formalizations available for set-theoretic developments, we present an automated translation of theories from Isabelle/HOL to Isabelle/ZF. This covers all fundamental primitives, particularly type classes. The translation produces LCF-style theorems that are checked by Isabelle's inference kernel. Type checking is replaced by explicit reasoning about set membership.

• Alexander Krauss. Partial and nested recursive function definitions in higher-order logic. Journal of Automated Reasoning, 44(4):303–336, 2010. (DOI)

  Based on inductive definitions, we develop a tool that automates the definition of partial recursive functions in higher-order logic (HOL) and provides appropriate proof rules for reasoning about them. Termination is modeled by an inductive domain predicate which follows the structure of the recursion. Since a partial induction rule is available immediately, partial correctness properties can be proved before termination is established. It turns out that this modularity also facilitates termination arguments for total functions, in particular for nested recursions. Our tool is implemented as a definitional package extending Isabelle/HOL. Various extensions provide convenience to the user: pattern matching, default values, tail recursion, mutual recursion and currying.

• Alexander Krauss. Pattern minimization problems over recursive data types. In James Hook and Peter Thiemann, editors, International Conference on Functional Programming (ICFP 2008). ACM, 2008. (DOI)

  In the context of program verification in an interactive theorem prover, we study the problem of transforming function definitions with ML-style (possibly overlapping) pattern matching into minimal sets of independent equations. Since independent equations are valid unconditionally, they are better suited for the equational proof style using induction and rewriting, which is often found in proofs in theorem provers or on paper. We relate the problem to the well-known minimization problem for propositional DNF formulas and show that it is Sigma ₂^P-complete. We then develop a concrete algorithm to compute minimal patterns, which naturally generalizes the standard Quine-McCluskey procedure to the domain of term patterns.

• Lukas Bulwahn, Alexander Krauss, Florian Haftmann, Levent Erkök, and John Matthews. Imperative functional programming in Isabelle/HOL. In Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics (TPHOLs 2008), volume 5170 of Lecture Notes in Computer Science, pages 134–149. Springer Verlag, 2008. (DOI)

  We introduce a lightweight approach for reasoning about programs involving imperative data structures using the proof assistant Isabelle/HOL. It is based on shallow embedding of programs, a polymorphic heap model using enumeration encodings and type classes, and a state-exception monad similar to known counterparts from Haskell. Existing proof automation tools are easily adapted to provide a verification environment. The framework immediately allows for correct code generation to ML and Haskell. Two case studies demonstrate our approach: An array-based checker for resolution proofs, and a more efficient bytecode verifier.

• Lukas Bulwahn, Alexander Krauss, and Tobias Nipkow. Finding lexicographic orders for termination proofs in Isabelle/HOL. In K. Schneider and J. Brandt, editors, Theorem Proving in Higher Order Logics (TPHOLs 2007), volume 4732 of Lecture Notes in Computer Science, pages 38–53. Springer Verlag, 2007. (DOI)

  We present a simple method to formally prove termination of recursive functions by searching for lexicographic combinations of size measures. Despite its simplicity, the method turns out to be powerful enough to solve a large majority of termination problems encountered in daily theorem proving practice.

• Alexander Krauss. Certified size-change termination. In Frank Pfenning, editor, Automated Deduction (CADE-21), volume 4603 of Lecture Notes in Computer Science, pages 460–476. Springer Verlag, 2007. (DOI)

  We develop a formalization of the Size-Change Principle in Isabelle/HOL and use it to construct formally certified termination proofs for recursive functions automatically.

• Alexander Krauss. Partial recursive functions in higher-order logic. In Ulrich Furbach and Natarajan Shankar, editors, Automated Reasoning (IJCAR 2006), volume 4130 of Lecture Notes in Artificial Intelligence, pages 589–603. Springer Verlag, 2006. (DOI)

  Based on inductive definitions, we develop an automated tool for defining partial recursive functions in Higher-Order Logic and providing appropriate reasoning tools for them. Our method expresses termination in a uniform manner and includes a very general form of pattern matching, where patterns can be arbitrary expressions. Termination proofs can be deferred, limited to subsets of arguments and are interchangeable with other proofs about the function. We show that this approach can also facilitate termination arguments for total functions, in particular for nested recursions. We implemented our tool as a definitional specification mechanism for Isabelle/HOL.

Thesis

• Alexander Krauss: Automating Recursive Definitions and Termination Proofs in Higher-Order Logic. Dissertation. Technische Universität München, 2009

Others

• Alexander Krauss and Armin Heller. A mechanized proof reconstruction for SCNP termination (extended abstract). In International Workshop on Termination (WST'09), 2009.

  Ben-Amram and Codish described SCNP, a subclass of the size-change termination criterion SCT, which permits efficient certificate checking. Termination problems in this class have a global ranking function of a certain form, which can be found using SAT solving. This note describes an automated proof reconstruction for this certificate scheme, implemented in the theorem prover Isabelle/HOL.

• Alexander Krauss. Shallow dependency pairs. In Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar, editors, TPHOLs 2008: Emerging Trends Proceedings, 2008. Department of Electrical and Computer Engineering, Concordia University.

  We show how the dependency pair approach, commonly used to modularize termination proofs of rewrite systems, can be adapted to establish termination of recursive functions in a system like Isabelle/HOL or Coq. It turns out that all that is required are two simple lemmas about wellfoundedness.

• Alexander Krauss. Defining Recursive Functions in Isabelle/HOL. Part of the Isabelle documentation. http://isabelle.in.tum.de/doc/functions.pdf.
• Alexander Krauss. Programmverifikation mit Modulen und Axiomatischen Spezifikationen in VeriFun. Diploma Thesis, Technische Universität Darmstadt, 2005.