| Publication | Date of Publication | Type |
|---|
| Formalising geometric axioms for Minkowski spacetime and without-loss-of-generality theorems | 2024-12-17 | Paper |
Linear resources in Isabelle/HOL
Journal of Automated Reasoning | 2024-06-10 | Paper |
A pragmatic, scalable approach to correct-by-construction process composition using classical linear logic inference
Logic-Based Program Synthesis and Transformation | 2023-11-09 | Paper |
A pragmatic, scalable approach to correct-by-construction process composition using classical linear logic inference
Logic-Based Program Synthesis and Transformation | 2023-11-09 | Paper |
Machine Learning for Inductive Theorem Proving
Artificial Intelligence and Symbolic Computation | 2023-06-30 | Paper |
Correction to: ``Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
Journal of Automated Reasoning | 2023-06-14 | Paper |
Re-imagining the Isabelle archive of formal proofs
Lecture Notes in Computer Science | 2023-06-02 | Paper |
Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
Journal of Automated Reasoning | 2022-12-12 | Paper |
| scientific article; zbMATH DE number 6984221 (Why is no real title available?) | 2018-11-23 | Paper |
| WorkflowFM: a logic-based framework for formal process specification and composition | 2017-09-22 | Paper |
ProofScript: proof scripting for the masses
Theoretical Aspects of Computing – ICTAC 2016 | 2016-12-21 | Paper |
Type inference for ZFH
Lecture Notes in Computer Science | 2015-11-20 | Paper |
Integrating systems around the user: combining Isabelle, Maple, and QEPCAD in the prover's palette
Electronic Notes in Theoretical Computer Science | 2014-07-22 | Paper |
A combinator language for theorem discovery
Lecture Notes in Computer Science | 2012-09-07 | Paper |
Exploring the foundations of discrete analytical geometry in Isabelle/HOL
Automated Deduction in Geometry | 2011-11-25 | Paper |
An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time
Automated Deduction in Geometry | 2011-11-25 | Paper |
Composable discovery engines for interactive theorem proving
Interactive Theorem Proving | 2011-08-17 | Paper |
Automation for dependently typed functional programming
Fundamenta Informaticae | 2011-05-20 | Paper |
An Isabelle-like procedural mode for HOL Light
Logic for Programming, Artificial Intelligence, and Reasoning | 2010-10-12 | Paper |
Formalizing Hilbert's Grundlagen in Isabelle/Isar
Lecture Notes in Computer Science | 2010-05-07 | Paper |
Combining Isabelle and QEPCAD-B in the Prover’s Palette
Lecture Notes in Computer Science | 2009-01-27 | Paper |
A proof-centric approach to mathematical assistants
Journal of Applied Logic | 2007-02-20 | Paper |
Automated Deduction in Geometry
Lecture Notes in Computer Science | 2006-10-20 | Paper |
Theorem Proving in Higher Order Logics
Lecture Notes in Computer Science | 2005-08-18 | Paper |
| scientific article; zbMATH DE number 1746669 (Why is no real title available?) | 2002-06-09 | Paper |
| scientific article; zbMATH DE number 1670741 (Why is no real title available?) | 2001-11-11 | Paper |
scientific article; zbMATH DE number 1646230 (Why is no real title available?)
Distinguished Dissertations | 2001-09-16 | Paper |
Theorem proving in infinitesimal geometry
Logic Journal of the IGPL | 2001-06-26 | Paper |
| scientific article; zbMATH DE number 1421054 (Why is no real title available?) | 2001-01-11 | Paper |
Mechanizing Nonstandard Real Analysis
LMS Journal of Computation and Mathematics | 2000-09-25 | Paper |
| scientific article; zbMATH DE number 1303336 (Why is no real title available?) | 1999-11-16 | Paper |
