| Publication | Date of Publication | Type |
|---|
| Stateless HOL | 2021-03-03 | Paper |
Stateless HOL
(available as arXiv preprint) | 2021-03-03 | Paper |
Proof-checking Euclid
Annals of Mathematics and Artificial Intelligence | 2019-05-16 | Paper |
| A mathematical proof proved correct: the most efficient way to pack spheres | 2017-05-18 | Paper |
A probabilistic analysis of the Game of the Goose
SIAM Review | 2016-05-20 | Paper |
Pollack-inconsistency
Electronic Notes in Theoretical Computer Science | 2014-07-22 | Paper |
A logical framework with explicit conversions
Electronic Notes in Theoretical Computer Science | 2014-01-10 | Paper |
Separation logic for non-local control flow and block scope variables
Lecture Notes in Computer Science | 2013-03-18 | Paper |
A synthesis of the procedural and declarative styles of interactive theorem proving
Logical Methods in Computer Science | 2012-04-03 | Paper |
A formalization of the C99 standard in HOL, Isabelle and Coq
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Proviola: a tool for proof re-animation
Lecture Notes in Computer Science | 2010-08-24 | Paper |
First order logic with domain conditions
Lecture Notes in Computer Science | 2010-05-07 | Paper |
Formalizing Arrow's theorem
Sādhanā | 2009-11-23 | Paper |
Merging Procedural and Declarative Proof
Lecture Notes in Computer Science | 2009-07-02 | Paper |
The challenge of computer mathematics
Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences | 2009-01-20 | Paper |
| scientific article; zbMATH DE number 5486212 (Why is no real title available?) | 2009-01-07 | Paper |
Mizar’s Soft Type System
Lecture Notes in Computer Science | 2008-09-02 | Paper |
Certified Computer Algebra on Top of an Interactive Theorem Prover
Towards Mechanized Mathematical Assistants | 2007-11-28 | Paper |
The meaning of infinity in calculus and computer algebra systems
Journal of Symbolic Computation | 2007-10-19 | Paper |
Constructive analysis, types and exact real numbers
Mathematical Structures in Computer Science | 2007-04-12 | Paper |
Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics
Journal of Applied Logic | 2007-02-20 | Paper |
Types for Proofs and Programs
Lecture Notes in Computer Science | 2005-12-23 | Paper |
Mathematical Knowledge Management
Lecture Notes in Computer Science | 2005-08-26 | Paper |
Theorem Proving in Higher Order Logics
Lecture Notes in Computer Science | 2005-08-18 | Paper |
| scientific article; zbMATH DE number 2090052 (Why is no real title available?) | 2004-08-12 | Paper |
| scientific article; zbMATH DE number 2085169 (Why is no real title available?) | 2004-08-09 | Paper |
A constructive algebraic hierarchy in Coq.
Journal of Symbolic Computation | 2003-08-21 | Paper |
| scientific article; zbMATH DE number 1951639 (Why is no real title available?) | 2003-07-21 | Paper |
A new implementation of Automath
Journal of Automated Reasoning | 2003-04-27 | Paper |
A comparison of Mizar and Isar
Journal of Automated Reasoning | 2003-04-27 | Paper |
| scientific article; zbMATH DE number 1863397 (Why is no real title available?) | 2003-02-04 | Paper |
| scientific article; zbMATH DE number 1670742 (Why is no real title available?) | 2001-11-11 | Paper |
UNIFORM ALGEBRAIC SPECIFICATIONS OF FINITE SETS WITH EQUALITY
International Journal of Foundations of Computer Science | 1992-06-28 | Paper |
| scientific article; zbMATH DE number 3821868 (Why is no real title available?) | 1983-01-01 | Paper |
