Jeremy Avigad

  • Carnegie Mellon University

According to our database1, Jeremy Avigad authored at least 67 papers between 1996 and 2022.

Collaborative distances:



In proceedings 
PhD thesis 


Online presence:



A verified algebraic representation of cairo program execution.
Proceedings of the CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17, 2022

Reliability of mathematical inference.
Synth., 2021

An Impossible Asylum.
CoRR, 2021

Verified Optimization.
CoRR, 2021

Modularity in Mathematics.
Rev. Symb. Log., 2020

Preface: Selected Extended Papers from Interactive Theorem Proving 2018.
J. Autom. Reason., 2020

CoRR, 2020

Progress on a perimeter surveillance problem.
CoRR, 2020

Algorithmic barriers to representing conditional independence.
Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, 2019

Data Types as Quotients of Polynomial Functors.
Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

Introduction to Milestones in Interactive Theorem Proving.
J. Autom. Reason., 2018

On the computability of graphons.
CoRR, 2018

Erratum to: Interactive Theorem Proving.
Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

A metaprogramming framework for formal verification.
Proc. ACM Program. Lang., 2017

A Formally Verified Proof of the Central Limit Theorem.
J. Autom. Reason., 2017

Character and Object.
Rev. Symb. Log., 2016

A Heuristic Prover for Real Inequalities.
J. Autom. Reason., 2016

Homotopy limits in type theory.
Math. Struct. Comput. Sci., 2015

Elaboration in Dependent Type Theory.
CoRR, 2015

The Lean Theorem Prover (System Description).
Proceedings of the Automated Deduction - CADE-25, 2015

Formally verified mathematics.
Commun. ACM, 2014

Thomas Hales. Dense Sphere Packings: A Blueprint for Formal Proofs. Cambridge University Press, Cambridge, 2012, xiv + 271 pp.
Bull. Symb. Log., 2014

Computability and analysis: the legacy of Alan Turing.
Proceedings of the Turing's Legacy: Developments from Turing's Ideas in Logic, 2014

Uniform distribution and algorithmic randomness.
J. Symb. Log., 2013

Homotopy limits in Coq
CoRR, 2013

A Machine-Checked Proof of the Odd Order Theorem.
Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

Uncomputably Noisy Ergodic Limits.
Notre Dame J. Formal Log., 2012

A metastable dominated convergence theorem.
J. Log. Anal., 2012

Type Inference in Mathematics.
Bull. EATCS, 2012

Computability and analysis: the legacy of Alan Turing
CoRR, 2012

Delta-Complete Decision Procedures for Satisfiability over the Reals
CoRR, 2012

Algorithmic randomness, reverse mathematics, and the dominated convergence theorem.
Ann. Pure Appl. Log., 2012

Bondy's Theorem.
Arch. Formal Proofs, 2012

Delta-Decidability over the Reals.
Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

δ-Complete Decision Procedures for Satisfiability over the Reals.
Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

Zen and the art of formalisation.
Math. Struct. Comput. Sci., 2011

Building a push-button RESOLVE verifier: Progress and challenges.
Formal Aspects Comput., 2011

<i>Handbook of Practical Logic and Automated Reasoning</i>, John Harrison, Cambridge University Press, 2009. Hardcover, ISBN-13: 978-0-521-89957-4, 681 pp. + xix, $135.00.
Theory Pract. Log. Program., 2010

A Formal System for Euclid's Elements.
Rev. Symb. Log., 2009

Functional interpretation and inductive definitions.
J. Symb. Log., 2009

The metamathematics of ergodic theory.
Ann. Pure Appl. Log., 2009

A language for mathematical language management
CoRR, 2008

A formally verified proof of the prime number theorem.
ACM Trans. Comput. Log., 2007

Quantifier elimination for the reals with a predicate for the powers of two.
Theor. Comput. Sci., 2007

A Decision Procedure for Linear "Big O" Equations.
J. Autom. Reason., 2007

Mathematical Method and Proof.
Synth., 2006

Combining decision procedures for the reals.
Log. Methods Comput. Sci., 2006

Fundamental notions of analysis in subsystems of second-order arithmetic.
Ann. Pure Appl. Log., 2006

Ann. Pure Appl. Log., 2005

Forcing in proof theory.
Bull. Symb. Log., 2004

Formalizing O Notation in Isabelle/HOL.
Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

Eliminating definitions and Skolem functions in first-order logic.
ACM Trans. Comput. Log., 2003

Erratum to "Saturated models of universal theories": [Ann. Pure Appl. Logic 118 (2002) 219-234].
Ann. Pure Appl. Log., 2003

Update Procedures and the 1-Consistency of Arithmetic.
Math. Log. Q., 2002

An Ordinal Analysis of Admissible Set Theory using Recursion on Ordinal Notations.
J. Math. Log., 2002

Saturated models of universal theories.
Ann. Pure Appl. Log., 2002

Transfer principles in nonstandard intuitionistic arithmetic.
Arch. Math. Log., 2002

Review of "Basic proof theory: second edition" by A. S. Troelstra and H. Schwichtenberg. Cambridge University Press.
SIGACT News, 2001

Algebraic proofs of cut elimination.
J. Log. Algebraic Methods Program., 2001

Interpreting Classical Theories in Constructive Ones.
J. Symb. Log., 2000

The Model-Theoretic Ordinal Analysis of Theories of Predicative Strength.
J. Symb. Log., 1999

Predicative Functionals and an Interpretation of ID<sub><omega</sub>.
Ann. Pure Appl. Log., 1998

An effective proof that open sets are Ramsey.
Arch. Math. Log., 1998

A model-theoretic approach to ordinal analysis.
Bull. Symb. Log., 1997

On the Relationship Between ATR<sub>0</sub> and ID<sub><omega</sub>.
J. Symb. Log., 1996

Formalizing Forcing Arguments in Subsystems of Second-Order Arithmetic.
Ann. Pure Appl. Log., 1996

Plausibly hard combinatorial tautologies.
Proceedings of the Proof Complexity and Feasible Arithmetics, 1996