Publication | Date of Publication | Type |
---|
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 |
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 |
Combining matching algorithms: The regular case | 2022-12-09 | Paper |
Modular higher-order E-unification | 2022-12-09 | Paper |
Verified Root-Balanced Trees | 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 analysis of random binary tree structures | 2018-10-04 | Paper |
Verified memoization and dynamic programming | 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 |
https://portal.mardi4nfdi.de/entity/Q3400637 | 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 |
https://portal.mardi4nfdi.de/entity/Q5435635 | 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 |
https://portal.mardi4nfdi.de/entity/Q2752051 | 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 |
Term rewriting and beyond -- theorem proving in Isabelle | 1989-01-01 | Paper |
Boolean unification - the story so far | 1989-01-01 | Paper |
Equational reasoning in Isabelle | 1989-01-01 | Paper |
Unification in Boolean rings | 1988-01-01 | Paper |
https://portal.mardi4nfdi.de/entity/Q3789063 | 1988-01-01 | Paper |
https://portal.mardi4nfdi.de/entity/Q3816965 | 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 |