| Publication | Date of Publication | Type |
|---|
| POSIX lexing with bitcoded derivatives | 2024-11-26 | Paper |
POSIX lexing with derivatives of regular expressions
Journal of Automated Reasoning | 2023-08-04 | Paper |
Priority inheritance protocol proved correct
Journal of Automated Reasoning | 2020-03-03 | Paper |
POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)
Interactive Theorem Proving | 2016-10-27 | Paper |
Mechanizing the metatheory of LF
ACM Transactions on Computational Logic | 2015-09-17 | Paper |
A formalisation of the Myhill-Nerode theorem based on regular expressions
Journal of Automated Reasoning | 2015-06-23 | Paper |
Revisiting Zucker's work on the correspondence between cut-elimination and normalisation
Trends in Logic | 2015-05-22 | Paper |
Formal SOS-Proofs for the Lambda-Calculus
Electronic Notes in Theoretical Computer Science | 2015-03-18 | Paper |
A Formal Model and Correctness Proof for an Access Control Policy Framework
Certified Programs and Proofs | 2015-01-13 | Paper |
| A head-to-head comparison of de Bruijn indices and names | 2014-01-10 | Paper |
| Formalising in nominal Isabelle Crary's completeness proof for equivalence checking | 2014-01-10 | Paper |
Mechanising Turing machines and computability theory in Isabelle/HOL
Interactive Theorem Proving | 2013-08-07 | Paper |
Priority inheritance protocol proved correct
Interactive Theorem Proving | 2012-09-20 | Paper |
General bindings and alpha-equivalence in Nominal Isabelle
Logical Methods in Computer Science | 2012-07-03 | Paper |
Mechanizing the metatheory of mini-XQuery
Certified Programs and Proofs | 2011-11-22 | Paper |
A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)
Interactive Theorem Proving | 2011-08-17 | Paper |
General bindings and alpha-equivalence in Nominal Isabelle
Programming Languages and Systems | 2011-05-19 | Paper |
A new foundation for Nominal Isabelle
Interactive Theorem Proving | 2010-09-14 | Paper |
| Nominal verification of algorithm \(W\) | 2010-02-05 | Paper |
A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
Automated Reasoning | 2009-03-12 | Paper |
Barendregt’s Variable Convention in Rule Inductions
Automated Deduction – CADE-21 | 2009-03-06 | Paper |
Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle
Lecture Notes in Computer Science | 2009-01-27 | Paper |
Nominal Inversion Principles
Lecture Notes in Computer Science | 2008-12-04 | Paper |
Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof
Rewriting Techniques and Applications | 2008-08-28 | Paper |
Nominal techniques in Isabelle/HOL
Journal of Automated Reasoning | 2008-06-11 | Paper |
Computer Science Logic
Lecture Notes in Computer Science | 2007-06-21 | Paper |
Categorical proof theory of classical propositional calculus
Theoretical Computer Science | 2007-01-09 | Paper |
Automated Deduction – CADE-20
Lecture Notes in Computer Science | 2006-11-01 | Paper |
Typed Lambda Calculi and Applications
Lecture Notes in Computer Science | 2005-11-11 | Paper |
Logic Programming
Lecture Notes in Computer Science | 2005-08-26 | Paper |
Nominal unification
Theoretical Computer Science | 2004-10-01 | Paper |
Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation
Journal Of Logic And Computation | 2004-01-28 | Paper |
| scientific article; zbMATH DE number 1722668 (Why is no real title available?) | 2002-03-21 | Paper |
