Jeremy Avigad

Affiliations:
  • Carnegie Mellon University


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

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2022
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

2021
Reliability of mathematical inference.
Synth., 2021

An Impossible Asylum.
CoRR, 2021

Verified Optimization.
CoRR, 2021

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

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

Foundations.
CoRR, 2020

Progress on a perimeter surveillance problem.
CoRR, 2020

2019
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

2018
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

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

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

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

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

2015
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

2014
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

2013
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

2012
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

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

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

2010
<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

2009
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

2008
A language for mathematical language management
CoRR, 2008

2007
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

2006
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

2005
Preface.
Ann. Pure Appl. Log., 2005

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

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

2003
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

2002
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

2001
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

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

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

1998
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

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

1996
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


  Loading...