I am a former member of the Theorem Proving Group at TUM, headed by Tobias Nipkow, working on the Isabelle theorem prover. In my dissertation I developed a defininition mechanism for recursive functions, and methods to prove termination of such functions automatically.

I left TUM in August 2011, and now work as a Principal Software Architect at QAware GmbH, designing and building business software for corporate customers.

Currently (April - September 2019), I am spending a research sabbatical at TUM. I am working to develop a soft type system on top of a set-theoretic logic.

Journal

• Ana Bove, Alexander Krauss, Matthieu Sozeau. Partiality and recursion in interactive theorem provers: An overview. Mathematical Structures in Computer Science 26(1): 38-88, 2016. PDF DOI
• Alexander Krauss, Tobias Nipkow. Proof Pearl: Regular expression equivalence and relation algebra. Journal of Automated Reasoning, 49(1):95–106, 2012. PDF DOI
• Jasmin Christian Blanchette, Alexander Krauss. Monotonicity inference for higher-order formulas. Journal of Automated Reasoning, 47(4): 369–398, 2011. PDF DOI
• Alexander Krauss. Partial and nested recursive function definitions in higher-order logic. Journal of Automated Reasoning, 44(4):303–336, 2010. PDF DOI

Conference

• Fabian Huch, Mojdeh Golagha, Ana Petrovska, Alexander Krauss. Machine learning-based run-time anomaly detection in software systems: An industrial evaluation. Machine Learning Techniques for Software Quality Evaluation (MaLTeSQuE 2018), 2018. PDF DOI
• Florian Haftmann, Alexander Krauss, Ondrej Kuncar, Tobias Nipkow. Data refinement in Isabelle/HOL. Interactive Theorem Proving (ITP 2013), 2013. PDF DOI
• Alexander Krauss, Cezary Kaliszyk. Scalable LCF-style proof translation. Interactive Theorem Proving (ITP 2013), 2013. PDF DOI
• Alexander Krauss, Christian Sternagel, René Thiemann, Carsten Fuhs, Jürgen Giesl. Termination of Isabelle functions via termination of rewriting. Interactive Theorem Proving (ITP 2011), 2011. PDF DOI
• Alexander Krauss, Andreas Schropp. A mechanized translation from higher-order logic to set theory. Interactive Theorem Proving (ITP 2010), 2010. PDF DOI
• Alexander Krauss. Recursive definitions of monadic functions. Partiality and Recursion in Interactive Theorem Proving (PAR 2010), 2010. PDF DOI
• Jasmin Christian Blanchette, Alexander Krauss. Monotonicity inference for higher-order formulas. Automated Reasoning (IJCAR 2010), 2010. PDF DOI
• Lukas Bulwahn, Alexander Krauss, Florian Haftmann, Levent Erkök, John Matthews. Imperative functional programming in Isabelle/HOL. Theorem Proving in Higher-Order Logics (TPHOLs 2008), 2008. PDF DOI
• Alexander Krauss. Pattern minimization problems over recursive data types. International Conference on Functional Programming (ICFP 2008), 2008. PDF DOI
• Alexander Krauss. Certified size-change termination. Automated Deduction (CADE 2007), 2007. PDF DOI
• Lukas Bulwahn, Alexander Krauss, Tobias Nipkow. Finding lexicographic orders for termination proofs in Isabelle/HOL. Theorem Proving in Higher-Order Logics (TPHOLs 2007), 2007. PDF DOI
• Alexander Krauss. Partial recursive functions in higher-order logic. Automated Reasoning (IJCAR 2006), 2006. PDF DOI

Thesis

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

Other

• Alexander Krauss. Adding soft types to Isabelle. Unpublished internal note, 2010. PDF
• Alexander Krauss, Armin Heller. A mechanized proof reconstruction for SCNP termination (extended abstract). In International Workshop on Termination (WST’09), 2009. PDF
• 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., 2008. PDF
• Alexander Krauss. Programmverifikation mit Modulen und Axiomatischen Spezifikationen in VeriFun. Diploma Thesis, Technische Universität Darmstadt, 2005. PDF

• krauss@in.tum.de