Fachartikel

Finding lexicographic orders for termination proofs in Isabelle/HOL

 |  Alexander Krauss

In: K. Schneider and J. Brandt, editors, Theorem Proving in Higher Order Logics (TPHOLs 2007) (Lukas Bulwahn, Alexander Krauss, and Tobias Nipkow) PDF

Ein Beitrag von
Machine learning-based run-time anomaly detection in software systems: An industrial evaluation

Machine Learning Techniques for Software Quality Evaluation (MaLTeSQuE), 2018 (Fabian Huch, Mojdeh Golagha, Ana Petrovska, Alexander Krauss)

Mehr Informationen
Ein Beitrag von
Partiality and recursion in interactive theorem provers: An overview

In: Mathematical Structures in Computer Science, 26(1), 2016. (Ana Bove, Alexander Krauss, Matthieu Sozeau) zum Artikel

Mehr Informationen
Ein Beitrag von
Proof pearl: Regular expression equivalence and relation algebra

In: Interactive Theorem Proving (ITP 2013), volume 7998 of Lecture Notes in Computer Science, pages 100–115. Springer Verlag, 2013. (Alexander[...]

Mehr Informationen
Ein Beitrag von
Scalable LCF-style proof translation

In: Interactive Theorem Proving (ITP 2013), volume 7998 of Lecture Notes in Computer Science, pages 100–115. Springer Verlag, 2013. (Alexander[...]

Mehr Informationen
Ein Beitrag von
Data refinement in Isabelle/HOL

In: Interactive Theorem Proving (ITP 2013), volume 7998 of Lecture Notes in Computer Science, pages 100–115. Springer Verlag, 2013. (Alexander[...]

Mehr Informationen
Ein Beitrag von
Invited Talk: Formalized Regular Expression Equivalence and Relation Algebra (in Isabelle/HOL)

International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 13), Cambridge, September 2012 (Alexander Krauss)

Mehr Informationen
Ein Beitrag von
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) (Alexander Krauss, Christian[...]

Mehr Informationen
Ein Beitrag von
Monotonicity inference for higher-order formulas

In: Journal of Automated Reasoning, 47(4), 2011 (Jasmin Christian Blanchette and Alexander Krauss) PDF

Mehr Informationen
Ein Beitrag von
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)[...]

Mehr Informationen
Ein Beitrag von
A mechanized translation from higher-order logic to set theory

In: Matt Kaufmann and Lawrence C. Paulson, editors, Interactive Theorem Proving (ITP 2010) (Alexander Krauss and Andreas Schopp) PDF

Mehr Informationen
Ein Beitrag von
Partial and nested recursive function definitions in higher-order logic

In: Journal of Automated Reasoning (Alexander Krauss) PDF

Mehr Informationen
Ein Beitrag von
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) (Lukas Bulwahn,[...]

Mehr Informationen
Ein Beitrag von
Pattern minimization problems over recursive data types

In: James Hook and Peter Thiemann, editors, International Conference on Functional Programming (ICFP 2008) (Alexander Krauss) PDF

Mehr Informationen
Ein Beitrag von
Certified size-change termination

In: Frank Pfenning, editor, Automated Deduction (CADE-21) (Alexander Krauss) zum Artikel

Mehr Informationen
Ein Beitrag von
Finding lexicographic orders for termination proofs in Isabelle/HOL

In: K. Schneider and J. Brandt, editors, Theorem Proving in Higher Order Logics (TPHOLs 2007) (Lukas Bulwahn, Alexander Krauss, and[...]

Mehr Informationen
Ein Beitrag von
Partial recursive functions in higher-order logic

In: Ulrich Furbach and Natarajan Shankar, editors, Automated Reasoning (IJCAR 2006) (Alexander Krauss) PDF

Mehr Informationen