| Publication | Date of Publication | Type |
|---|
| Real-time double-ended queue verified (proof pearl) | 2024-11-26 | Paper |
| Gale-Shapley verified | 2024-09-27 | Paper |
| Formal verification of algorithm \(\mathcal{W}\): the monomorphic case | 2024-07-05 | Paper |
| Winskel is (almost) right. Towards a mechanized semantics textbook | 2024-07-05 | Paper |
| Verification of NP-Hardness Reduction Functions for Exact Lattice Problems | 2024-04-26 | Paper |
| I/O automata in Isabelle/HOL | 2023-12-08 | Paper |
| https://portal.mardi4nfdi.de/entity/Q6060676 | 2023-11-03 | Paper |
| A verified implementation of \(\mathrm{B}^+\)-trees in Isabelle/HOL | 2023-07-28 | Paper |
| Ordered rewriting and confluence | 2023-04-28 | Paper |
| Higher-order unification, polymorphism, and subsorts | 2023-03-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5875432 | 2023-02-03 | Paper |
| Verified Textbook Algorithms | 2022-12-22 | Paper |
| A formalization and proof checker for Isabelle's metalogic | 2022-12-19 | Paper |
| Verified Root-Balanced Trees | 2022-12-09 | Paper |
| Modular higher-order E-unification | 2022-12-09 | Paper |
| Combining matching algorithms: The regular case | 2022-12-09 | Paper |
| Verified Approximation Algorithms | 2022-11-09 | Paper |
| Verification of Closest Pair of Points Algorithms | 2022-11-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5094121 | 2022-08-02 | Paper |
| Trustworthy Graph Algorithms (Invited Talk) | 2022-07-21 | Paper |
| A verified decision procedure for orders in Isabelle/HOL | 2022-06-22 | Paper |
| Isabelle's metalogic: formalization and proof checker | 2021-12-01 | Paper |
| Verified analysis of random binary tree structures | 2020-11-02 | Paper |
| From LCF to Isabelle/HOL | 2019-12-18 | Paper |
| Formal verification of language-based concurrent noninterference | 2019-09-18 | Paper |
| Hoare logics for time bounds. A study in meta theory | 2019-09-16 | Paper |
| A verified compiler from Isabelle/HOL to CakeML | 2019-09-13 | Paper |
| Amortized complexity verified | 2019-03-20 | Paper |
| More Church-Rosser proofs (in Isabelle/HOL) | 2019-01-15 | Paper |
| Verified memoization and dynamic programming | 2018-10-04 | Paper |
| Verified analysis of random binary tree structures | 2018-10-04 | Paper |
| Verified Analysis of List Update Algorithms. | 2018-04-19 | Paper |
| Verified decision procedures for MSO on words based on derivatives of regular expressions | 2017-10-23 | Paper |
| Automatic Functional Correctness Proofs for Functional Search Trees | 2016-10-27 | Paper |
| A Verified Compiler for Probability Density Functions | 2016-04-26 | Paper |
| Mining the Archive of Formal Proofs | 2015-11-20 | Paper |
| Amortized Complexity Verified | 2015-09-14 | Paper |
| Verified decision procedures for MSO on words based on derivatives of regular expressions | 2015-03-30 | Paper |
| Formalizing Probabilistic Noninterference | 2015-01-13 | Paper |
| Concrete Semantics | 2014-10-23 | Paper |
| Unified Decision Procedures for Regular Expression Equivalence | 2014-09-08 | Paper |
| A Brief Survey of Verified Decision Procedures for Equivalence of Regular Expressions | 2013-10-04 | Paper |
| Noninterfering Schedulers | 2013-09-13 | Paper |
| Data Refinement in Isabelle/HOL | 2013-08-07 | Paper |
| Proof Pearl: regular expression equivalence and relation algebra | 2013-08-01 | Paper |
| Proving Concurrent Noninterference | 2013-04-19 | Paper |
| A compiled implementation of normalisation by evaluation | 2012-09-21 | Paper |
| Abstract Interpretation of Annotated Commands | 2012-09-20 | Paper |
| Verifying pCTL Model Checking | 2012-06-29 | Paper |
| Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs | 2012-06-15 | Paper |
| Proof Pearl: The Marriage Theorem | 2011-11-22 | Paper |
| Automatic Proof and Disproof in Isabelle/HOL | 2011-10-07 | Paper |
| Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism | 2011-08-17 | Paper |
| Linear quantifier elimination | 2010-10-08 | Paper |
| Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder | 2010-09-14 | Paper |
| Sledgehammer: Judgement Day | 2010-09-14 | Paper |
| Code Generation via Higher-Order Rewrite Systems | 2010-05-04 | Paper |
| Automated Deduction – CADE-19 | 2010-04-20 | Paper |
| Flyspeck II: The basic linear programs | 2010-03-19 | Paper |
| Nominal verification of algorithm \(W\) | 2010-02-05 | Paper |
| Social choice theory in HOL. Arrow and Gibbard-Satterthwaite | 2010-01-25 | Paper |
| Flyspeck I: Tame Graphs | 2009-03-12 | Paper |
| The Isabelle Framework | 2008-12-04 | Paper |
| A Compiled Implementation of Normalization by Evaluation | 2008-12-04 | Paper |
| Linear Quantifier Elimination | 2008-11-27 | Paper |
| Verifying a Hotel Key Card System | 2008-09-11 | Paper |
| Proof synthesis and reflection for linear arithmetic | 2008-09-10 | Paper |
| Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL | 2008-09-02 | Paper |
| Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic | 2008-05-27 | Paper |
| Jinja: towards a comprehensive formal semantics for a Java-like language | 2008-01-14 | Paper |
| Theorem Proving in Higher Order Logics | 2006-07-06 | Paper |
| Programming Languages and Systems | 2005-09-13 | Paper |
| Theorem Proving in Higher Order Logics | 2005-08-18 | Paper |
| Proving pointer programs in higher-order logic | 2005-08-05 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4673417 | 2005-04-29 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4823141 | 2004-10-26 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4808824 | 2004-08-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4736387 | 2004-08-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4470494 | 2004-07-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4435474 | 2003-11-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4411818 | 2003-07-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4484332 | 2003-06-12 | Paper |
| Verified bytecode verifiers. | 2003-05-25 | Paper |
| \(\mu\)Java: Embedding a programming language in a theorem prover | 2002-10-23 | Paper |
| Isabelle/HOL. A proof assistant for higher-order logic | 2002-06-12 | Paper |
| Verified lightweight bytecode verification | 2002-05-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2769440 | 2002-02-05 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2754030 | 2001-11-11 | Paper |
| More Church-Rosser proofs (in Isabelle/HOL) | 2001-02-18 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4524793 | 2001-01-15 | Paper |
| Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L | 2000-09-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4246952 | 1999-12-13 | Paper |
| Term Rewriting and All That | 1999-12-13 | Paper |
| HOLCF = HOL + LCF | 1999-11-29 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4264719 | 1999-10-07 | Paper |
| Winskel is (almost) right: Towards a mechanized semantics textbook | 1999-01-03 | Paper |
| Higher-order rewrite systems and their confluence | 1998-08-13 | Paper |
| Type Reconstruction for Type Classes | 1995-10-09 | Paper |
| Reduction and unification in lambda calculi with a general notion of subtype | 1994-12-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4281481 | 1994-03-10 | Paper |
| Combining matching algorithms: The regular case | 1992-06-28 | Paper |
| Unification in primal algebras, their powers and their varieties | 1990-01-01 | Paper |
| Equational reasoning in Isabelle | 1989-01-01 | Paper |
| Boolean unification - the story so far | 1989-01-01 | Paper |
| Term rewriting and beyond -- theorem proving in Isabelle | 1989-01-01 | Paper |
| Unification in Boolean rings | 1988-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3816965 | 1988-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3789063 | 1988-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4725724 | 1987-01-01 | Paper |
| Non-deterministic data types: Models and implementations | 1986-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3786022 | 1986-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3956381 | 1982-01-01 | Paper |
