Jeremy Avigad

According to our database, Jeremy Avigad authored at least 77 papers between 1996 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of two.

2024

ImProver: Agent-Based Automated Proof Optimization.

Riyaz Ahuja, Jeremy Avigad, Prasad Tetali, Sean Welleck

CoRR, 2024

Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory.

Joshua Clune, Yicheng Qian, Alexander Bentkamp, Jeremy Avigad

Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

Automated Reasoning for Mathematics.

Jeremy Avigad

Proceedings of the Automated Reasoning - 12th International Joint Conference, 2024

2023

Two-Sorted Frege Arithmetic is not conservative.

Stephen Mackereth, Jeremy Avigad

Rev. Symb. Log., December, 2023

An Impossible Asylum.

Jeremy Avigad, Seulkee Baek, Alexander Bentkamp, Marijn Heule, Wojciech Nawrocki

Am. Math. Mon., May, 2023

ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics.

Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, Jeremy Avigad

CoRR, 2023

Verified reductions for optimization.

Alexander Bentkamp, Ramon Fernández Mir, Jeremy Avigad

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

Certified Knowledge Compilation with Application to Verified Model Counting.

Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, Marijn J. H. Heule

Proceedings of the 26th International Conference on Theory and Applications of Satisfiability Testing, 2023

A Proof-Producing Compiler for Blockchain Applications.

Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman

Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023

Verified Encodings for SAT Solvers.

Cayden R. Codel, Jeremy Avigad, Marijn J. H. Heule

Proceedings of the Formal Methods in Computer-Aided Design, 2023

2022

A verified algebraic representation of cairo program execution.

Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman

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.

Jeremy Avigad

Synth., 2021

Verified Optimization.

Alexander Bentkamp, Jeremy Avigad

CoRR, 2021

Verified Optimization (work in progress).

Alexander Bentkamp, Jeremy Avigad

Proceedings of the Joint Proceedings of the FMM, FVPS, MathUI,NatFoM, and OpenMath Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2021 co-located with the 14th Conference on Intelligent Computer Mathematics (CICM 2021), Virtual Event, Timisoara, Romania, July 26, 2021

2020

Modularity in Mathematics.

Jeremy Avigad

Rev. Symb. Log., 2020

Preface: Selected Extended Papers from Interactive Theorem Proving 2018.

Jeremy Avigad, Assia Mahboubi

J. Autom. Reason., 2020

Foundations.

Jeremy Avigad

CoRR, 2020

Progress on a perimeter surveillance problem.

Jeremy Avigad, Floris van Doorn

CoRR, 2020

2019

Algorithmic barriers to representing conditional independence.

Nathanael L. Ackerman, Jeremy Avigad, Cameron E. Freer, Daniel M. Roy, Jason M. Rute

Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, 2019

Data Types as Quotients of Polynomial Functors.

Jeremy Avigad, Mario Carneiro, Simon Hudon

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

2018

Introduction to Milestones in Interactive Theorem Proving.

Jeremy Avigad, Jasmin Christian Blanchette, Gerwin Klein, Lawrence C. Paulson, Andrei Popescu, Gregor Snelting

J. Autom. Reason., 2018

On the computability of graphons.

Nathanael L. Ackerman, Jeremy Avigad, Cameron E. Freer, Daniel M. Roy, Jason M. Rute

CoRR, 2018

Erratum to: Interactive Theorem Proving.

Jeremy Avigad, Assia Mahboubi

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

2017

A metaprogramming framework for formal verification.

Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura

Proc. ACM Program. Lang., 2017

A Formally Verified Proof of the Central Limit Theorem.

Jeremy Avigad, Johannes Hölzl, Luke Serafin

J. Autom. Reason., 2017

2016

Character and Object.

Jeremy Avigad, Rebecca Lea Morris

Rev. Symb. Log., 2016

A Heuristic Prover for Real Inequalities.

Jeremy Avigad, Robert Y. Lewis, Cody Roux

J. Autom. Reason., 2016

2015

Homotopy limits in type theory.

Jeremy Avigad, Krzysztof Kapulkin, Peter LeFanu Lumsdaine

Math. Struct. Comput. Sci., 2015

Elaboration in Dependent Type Theory.

Leonardo Mendonça de Moura, Jeremy Avigad, Soonho Kong, Cody Roux

CoRR, 2015

The Lean Theorem Prover (System Description).

Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer

Proceedings of the Automated Deduction - CADE-25, 2015

2014

Formally verified mathematics.

Jeremy Avigad, John Harrison

Commun. ACM, 2014

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

Jeremy Avigad

Bull. Symb. Log., 2014

Computability and analysis: the legacy of Alan Turing.

Jeremy Avigad, Vasco Brattka

Proceedings of the Turing's Legacy: Developments from Turing's Ideas in Logic, 2014

2013

Uniform distribution and algorithmic randomness.

Jeremy Avigad

J. Symb. Log., 2013

Homotopy limits in Coq

Jeremy Avigad, Krzysztof Kapulkin, Peter LeFanu Lumsdaine

CoRR, 2013

A Machine-Checked Proof of the Odd Order Theorem.

Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Théry

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2012

Uncomputably Noisy Ergodic Limits.

Jeremy Avigad

Notre Dame J. Formal Log., 2012

A metastable dominated convergence theorem.

Jeremy Avigad, Edward T. Dean, Jason M. Rute

J. Log. Anal., 2012

Type Inference in Mathematics.

Jeremy Avigad

Bull. EATCS, 2012

Computability and analysis: the legacy of Alan Turing

Jeremy Avigad, Vasco Brattka

CoRR, 2012

Delta-Complete Decision Procedures for Satisfiability over the Reals

Sicun Gao, Jeremy Avigad, Edmund M. Clarke

CoRR, 2012

Algorithmic randomness, reverse mathematics, and the dominated convergence theorem.

Jeremy Avigad, Edward T. Dean, Jason M. Rute

Ann. Pure Appl. Log., 2012

Bondy's Theorem.

Jeremy Avigad, Stefan Hetzl

Arch. Formal Proofs, 2012

Delta-Decidability over the Reals.

Sicun Gao, Jeremy Avigad, Edmund M. Clarke

Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

δ-Complete Decision Procedures for Satisfiability over the Reals.

Sicun Gao, Jeremy Avigad, Edmund M. Clarke

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

2011

Zen and the art of formalisation.

Andrea Asperti, Jeremy Avigad

Math. Struct. Comput. Sci., 2011

Building a push-button RESOLVE verifier: Progress and challenges.

Murali Sitaraman, Bruce M. Adcock, Jeremy Avigad, Derek Bronish, Paolo Bucci, David Frazier, Harvey M. Friedman, Heather K. Harton, Wayne D. Heym, Jason Kirschenbaum, Joan Krone, Hampton Smith, Bruce W. Weide

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.

Jeremy Avigad

Theory Pract. Log. Program., 2010

2009

A Formal System for Euclid's Elements.

Jeremy Avigad, Edward T. Dean, John Mumma

Rev. Symb. Log., 2009

Functional interpretation and inductive definitions.

Jeremy Avigad, Henry Towsner

J. Symb. Log., 2009

The metamathematics of ergodic theory.

Jeremy Avigad

Ann. Pure Appl. Log., 2009

2008

A language for mathematical language management

Steven Kieffer, Jeremy Avigad, Harvey Friedman

CoRR, 2008

2007

A formally verified proof of the prime number theorem.

Jeremy Avigad, Kevin Donnelly, David Gray, Paul Raff

ACM Trans. Comput. Log., 2007

Quantifier elimination for the reals with a predicate for the powers of two.

Jeremy Avigad, Yimu Yin

Theor. Comput. Sci., 2007

A Decision Procedure for Linear "Big O" Equations.

Jeremy Avigad, Kevin Donnelly

J. Autom. Reason., 2007

2006

Mathematical Method and Proof.

Jeremy Avigad

Synth., 2006

Combining decision procedures for the reals.

Jeremy Avigad, Harvey Friedman

Log. Methods Comput. Sci., 2006

Fundamental notions of analysis in subsystems of second-order arithmetic.

Jeremy Avigad, Ksenija Simic

Ann. Pure Appl. Log., 2006

2005

Preface.

Arnold Beckmann, Jeremy Avigad, Georg Moser

Ann. Pure Appl. Log., 2005

2004

Forcing in proof theory.

Jeremy Avigad

Bull. Symb. Log., 2004

Formalizing O Notation in Isabelle/HOL.

Jeremy Avigad, Kevin Donnelly

Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

2003

Eliminating definitions and Skolem functions in first-order logic.

Jeremy Avigad

ACM Trans. Comput. Log., 2003

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

Jeremy Avigad

Ann. Pure Appl. Log., 2003

2002

Update Procedures and the 1-Consistency of Arithmetic.

Jeremy Avigad

Math. Log. Q., 2002

An Ordinal Analysis of Admissible Set Theory using Recursion on Ordinal Notations.

Jeremy Avigad

J. Math. Log., 2002

Saturated models of universal theories.

Jeremy Avigad

Ann. Pure Appl. Log., 2002

Transfer principles in nonstandard intuitionistic arithmetic.

Jeremy Avigad, Jeremy Helzner

Arch. Math. Log., 2002

2001

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

Jeremy Avigad

SIGACT News, 2001

Algebraic proofs of cut elimination.

Jeremy Avigad

J. Log. Algebraic Methods Program., 2001

2000

Interpreting Classical Theories in Constructive Ones.

Jeremy Avigad

J. Symb. Log., 2000

1999

The Model-Theoretic Ordinal Analysis of Theories of Predicative Strength.

Jeremy Avigad, Richard Sommer

J. Symb. Log., 1999

1998

Predicative Functionals and an Interpretation of ID_<omega.

Jeremy Avigad

Ann. Pure Appl. Log., 1998

An effective proof that open sets are Ramsey.

Jeremy Avigad

Arch. Math. Log., 1998

1997

A model-theoretic approach to ordinal analysis.

Jeremy Avigad, Richard Sommer

Bull. Symb. Log., 1997

1996

On the Relationship Between ATR₀ and ID_<omega.

Jeremy Avigad

J. Symb. Log., 1996

Formalizing Forcing Arguments in Subsystems of Second-Order Arithmetic.

Jeremy Avigad

Ann. Pure Appl. Log., 1996

Plausibly hard combinatorial tautologies.

Jeremy Avigad

Proceedings of the Proof Complexity and Feasible Arithmetics, 1996