| Publication | Date of Publication | Type |
|---|
Algorithmic barriers to representing conditional independence
| 2024-12-19 | Paper |
A proof-producing compiler for blockchain applications
| 2024-11-26 | Paper |
Certified knowledge compilation with application to verified model counting
| 2024-11-26 | Paper |
What we talk about when we talk about mathematics
| 2024-10-24 | Paper |
Mathematics and language
| 2024-09-06 | Paper |
Verified reductions for optimization
| 2024-04-05 | Paper |
Mathematics and the formal turn
Bulletin of the American Mathematical Society | 2024-04-03 | Paper |
TWO-SORTED FREGE ARITHMETIC IS NOT CONSERVATIVE
The Review of Symbolic Logic | 2024-01-11 | Paper |
An Impossible Asylum
The American Mathematical Monthly | 2023-05-11 | Paper |
Reliability of mathematical inference
Synthese | 2023-03-31 | Paper |
Mathematical Logic and Computation
| 2022-08-01 | Paper |
Varieties of mathematical understanding
Bulletin of the American Mathematical Society | 2021-11-19 | Paper |
Foundations
| 2020-09-20 | Paper |
Modularity in mathematics
The Review of Symbolic Logic | 2020-03-25 | Paper |
Opinion: The Mechanization of Mathematics
Notices of the American Mathematical Society | 2018-11-02 | Paper |
A formally verified proof of the central limit theorem
Journal of Automated Reasoning | 2018-02-02 | Paper |
On the computability of graphons
| 2018-01-31 | Paper |
Proof Theory
| 2017-11-06 | Paper |
Eliminating definitions and Skolem functions in first-order logic
ACM Transactions on Computational Logic | 2017-06-13 | Paper |
Character and object
The Review of Symbolic Logic | 2017-05-31 | Paper |
\(\delta\)-decidability over the reals
2012 27th Annual IEEE Symposium on Logic in Computer Science | 2017-05-16 | Paper |
Logic's Lost Genius and Gentzen's Centenary
Notices of the American Mathematical Society | 2017-01-02 | Paper |
Homotopy limits in type theory
Mathematical Structures in Computer Science | 2016-07-27 | Paper |
Book review of: S. B. Cooper (ed.) and J. van Leeuwen (ed.), Alan Turing. His work and impact
Notices of the American Mathematical Society | 2016-06-15 | Paper |
A heuristic prover for real inequalities
Journal of Automated Reasoning | 2016-05-26 | Paper |
Book review of: T. C. Hales, Dense sphere packings. A blueprint for formal proofs
The Bulletin of Symbolic Logic | 2016-03-18 | Paper |
The Lean theorem prover (system description)
Automated Deduction - CADE-25 | 2015-12-02 | Paper |
Oscillation and the mean ergodic theorem for uniformly convex Banach spaces
Ergodic Theory and Dynamical Systems | 2015-07-13 | Paper |
A heuristic prover for real inequalities
Interactive Theorem Proving | 2014-09-08 | Paper |
The concept of ``character in Dirichlet's theorem on primes in an arithmetic progression
Archive for History of Exact Sciences | 2014-07-01 | Paper |
Ultraproducts and metastability
The New York Journal of Mathematics | 2014-03-14 | Paper |
Understanding, formal verification, and the philosophy of mathematics
| 2013-10-04 | Paper |
A machine-checked proof of the odd order theorem
Interactive Theorem Proving | 2013-08-07 | Paper |
Uniform distribution and algorithmic randomness
Journal of Symbolic Logic | 2013-04-23 | Paper |
Type inference in mathematics
| 2013-01-28 | Paper |
A metastable dominated convergence theorem
Journal of Logic and Analysis | 2012-12-17 | Paper |
Uncomputably noisy ergodic limits
Notre Dame Journal of Formal Logic | 2012-11-23 | Paper |
Algorithmic randomness, reverse mathematics, and the dominated convergence theorem
Annals of Pure and Applied Logic | 2012-10-11 | Paper |
\(\delta \)-complete decision procedures for satisfiability over the reals
Automated Reasoning | 2012-09-05 | Paper |
Inverting the Furstenberg correspondence
Discrete and Continuous Dynamical Systems | 2012-08-24 | Paper |
Computability and analysis: the legacy of Alan Turing
| 2012-06-15 | Paper |
Zen and the art of formalisation
Mathematical Structures in Computer Science | 2011-10-21 | Paper |
The computational content of classical arithmetic
| 2011-05-31 | Paper |
scientific article; zbMATH DE number 5859773 (Why is no real title available?)
| 2011-03-02 | Paper |
Metastability in the Furstenberg-Zimmer tower
Fundamenta Mathematicae | 2011-01-11 | Paper |
Local stability of ergodic averages
Transactions of the American Mathematical Society | 2010-02-02 | Paper |
A FORMAL SYSTEM FOR EUCLID’SELEMENTS
The Review of Symbolic Logic | 2010-01-21 | Paper |
Functional interpretation and inductive definitions
Journal of Symbolic Logic | 2010-01-07 | Paper |
The metamathematics of ergodic theory
Annals of Pure and Applied Logic | 2009-03-25 | Paper |
scientific article; zbMATH DE number 5204708 (Why is no real title available?)
| 2007-10-24 | Paper |
Combining decision procedures for the reals
Logical Methods in Computer Science | 2007-10-11 | Paper |
Automated Reasoning
Lecture Notes in Computer Science | 2007-09-25 | Paper |
A decision procedure for linear ``big O equations
Journal of Automated Reasoning | 2007-08-17 | Paper |
Quantifier elimination for the reals with a predicate for the powers of two
Theoretical Computer Science | 2007-02-26 | Paper |
Mathematical method and proof
Synthese | 2006-12-20 | Paper |
Fundamental notions of analysis in subsystems of second-order arithmetic
Annals of Pure and Applied Logic | 2006-04-28 | Paper |
scientific article; zbMATH DE number 2236625 (Why is no real title available?)
| 2005-12-08 | Paper |
Forcing in Proof Theory
The Bulletin of Symbolic Logic | 2005-05-24 | Paper |
Number theory and elementary arithmetic†
Philosophia Mathematica | 2004-06-10 | Paper |
Transfer principles in nonstandard intuitionistic arithmetic
Archive for Mathematical Logic | 2003-09-16 | Paper |
AN ORDINAL ANALYSIS OF ADMISSIBLE SET THEORY USING RECURSION ON ORDINAL NOTATIONS
Journal of Mathematical Logic | 2003-07-25 | Paper |
Saturated models of universal theories
Annals of Pure and Applied Logic | 2003-03-09 | Paper |
scientific article; zbMATH DE number 1870411 (Why is no real title available?)
| 2003-02-18 | Paper |
Update procedures and the 1-consistency of arithmetic
Mathematical Logic Quarterly (MLQ) | 2002-07-22 | Paper |
Algebraic proofs of cut elimination
The Journal of Logic and Algebraic Programming | 2002-05-21 | Paper |
Interpreting classical theories in constructive ones
The Journal of Symbolic Logic | 2002-03-11 | Paper |
scientific article; zbMATH DE number 1420833 (Why is no real title available?)
| 2000-10-22 | Paper |
Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\)
Annals of Pure and Applied Logic | 1999-08-16 | Paper |
The model-theoretic ordinal analysis of theories of predicative strength
Journal of Symbolic Logic | 1999-06-29 | Paper |
An effective proof that open sets are Ramsey
Archive for Mathematical Logic | 1999-03-25 | Paper |
scientific article; zbMATH DE number 1215497 (Why is no real title available?)
| 1998-12-08 | Paper |
scientific article; zbMATH DE number 1114014 (Why is no real title available?)
| 1998-07-08 | Paper |
A Model-Theoretic Approach to Ordinal Analysis
The Bulletin of Symbolic Logic | 1997-11-05 | Paper |
Formalizing forcing arguments in subsystems of second-order arithmetic
Annals of Pure and Applied Logic | 1997-01-26 | Paper |
On the relationship between ATR0 and
Journal of Symbolic Logic | 1996-12-12 | Paper |
