# Dr. Alexander Krauss

## Research Interests

Definition Principles
Isabelle Theorem Prover
Formal Methods
Functional Programming
HOL
Partial Functions
Pattern Matching
Program Verification
Recursion
Relation Algebra
Rewriting
Set Theory
Termination
Interactive Theorem Proving
Type Theory

I am a former member of the Theorem Proving Group, headed by Tobias Nipkow. My research interests are located somewhere in the cloud to the right. In my dissertation I developed a defininition mechanism for recursive functions in Isabelle, and methods to prove termination of such functions automatically.

I left TUM in August 2011, and now work at QAware GmbH.

## Publications

### Preprints

- Ana Bove, Alexander Krauss, and
Matthieu Sozeau.
Partiality and recursion in interactive theorem provers: An overview.
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 several 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 extent, 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

- Florian Haftmann, Alexander
Krauss, Ondrej Kuncar, and Tobias Nipkow.
Data
refinement in Isabelle/HOL.
In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors,
Interactive Theorem Proving (ITP 2013), volume 7998 of
Lecture Notes in Computer Science, pages 100–115. Springer
Verlag, 2013.
(DOI)
The paper shows how the code generator of Isabelle/HOL supports data refinement, i.e., providing efficient code for operations on abstract types, e.g., sets or numbers. This allows all tools that employ code generation, e.g., Quickcheck or proof by evaluation, to compute with these abstract types. At the core is an extension of the code generator to deal with data type invariants. In order to automate the process of setting up specific data refinements, two packages for transferring definitions and theorems between types are exploited.

- Cezary Kaliszyk and Alexander
Krauss.
Scalable
LCF-style proof translation.
In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors,
Interactive Theorem Proving (ITP 2013), volume 7998 of
Lecture Notes in Computer Science, pages 51–66. Springer
Verlag, 2013.
(DOI)
All existing translations between proof assistants have been notoriously sluggy, resource-demanding, and do not scale to large developments, which has lead to the general perception that the whole approach is probably not practical. We aim to show that the observed inefficiencies are not inherent, but merely a deficiency of the existing implementations. We do so by providing a new implementation of a theory import from HOL Light to Isabelle/HOL, which achieves decent performance and scalability mostly by avoiding the mistakes of the past. After some preprocessing, our tool can import large HOL Light developments faster than HOL Light processes them. Our main target and motivation is the Flyspeck development, which can be imported in a few hours on commodity hardware. We also provide mappings for most basic types present in the developments including lists, integers and real numbers. This papers outlines some design considerations and presents a few of our extensive measurements, which reveal interesting insights in the low-level structure of larger proof developments.

- Alexander Krauss and Tobias
Nipkow.
Proof pearl: Regular
expression equivalence and relation algebra.
Journal of Automated Reasoning, 49(1):95–106, 2012.
(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, 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.
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

_{2}^{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.

## Teaching

SS 2011: | Perlen der Informatik 2 | (Übungsleitung) |

WS 2010/11: | Semantics of Programming Languages | (Übungsleitung) |

SS 2010: | Einführung in die Theoretische Informatik | (Übungsleitung) |

SS 2009: | Einführung in die Theoretische Informatik | (Übungsleitung) |

WS 2008/09: | Logic | (Übungsleitung) |

SS 2008: | Einführung in die Theoretische Informatik | (Übungsleitung) |

WS 2007/08: | Perlen der Informatik | (Übungsleitung) |

SS 2007: | Perlen der Informatik 2 | (Übungsleitung) |

WS 2006/07: | Perlen der Informatik | (Übungsleitung) |