Jeremy Avigad

Publication Activity (10 Years)

Years Active: 1996-2024
Publications (10 Years): 31

Top Topics

Conditional Independencies

Top Venues

J. Autom. Reason.

Rev. Symb. Log.

Publications

Jeremy Avigad
Automated Reasoning for Mathematics. IJCAR (1) (2024)
Stephen Mackereth, Jeremy Avigad
Two-Sorted Frege Arithmetic is not conservative. Rev. Symb. Log. 16 (4) (2023)
Alexander Bentkamp, Ramon Fernández Mir, Jeremy Avigad
Verified reductions for optimization. CoRR (2023)
Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman
A Proof-Producing Compiler for Blockchain Applications. ITP (2023)
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, Jeremy Avigad
ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics. CoRR (2023)
Jeremy Avigad, Seulkee Baek, Alexander Bentkamp, Marijn Heule, Wojciech Nawrocki
An Impossible Asylum. Am. Math. Mon. 130 (5) (2023)
Cayden R. Codel, Jeremy Avigad, Marijn J. H. Heule
Verified Encodings for SAT Solvers. FMCAD (2023)
Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, Marijn J. H. Heule
Certified Knowledge Compilation with Application to Verified Model Counting. SAT (2023)
Alexander Bentkamp, Ramon Fernández Mir, Jeremy Avigad
Verified reductions for optimization. TACAS (2) (2023)
Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman
A verified algebraic representation of cairo program execution. CPP (2022)
Jeremy Avigad, Seulkee Baek, Alexander Bentkamp, Marijn Heule, Wojciech Nawrocki
An Impossible Asylum. CoRR (2021)
Alexander Bentkamp, Jeremy Avigad
Verified Optimization. CoRR (2021)
Alexander Bentkamp, Jeremy Avigad
Verified Optimization (work in progress). CICM Workshops (2021)
Jeremy Avigad
Reliability of mathematical inference. Synth. 198 (8) (2021)
Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman
A verified algebraic representation of Cairo program execution. CoRR (2021)
Jeremy Avigad, Floris van Doorn
Progress on a perimeter surveillance problem. CoRR (2020)
Jeremy Avigad, Assia Mahboubi
Preface: Selected Extended Papers from Interactive Theorem Proving 2018. J. Autom. Reason. 64 (5) (2020)
Jeremy Avigad
Modularity in Mathematics. Rev. Symb. Log. 13 (1) (2020)
Jeremy Avigad
Foundations. CoRR (2020)
Jeremy Avigad, Mario Carneiro, Simon Hudon
Data Types as Quotients of Polynomial Functors. ITP (2019)
Nathanael L. Ackerman, Jeremy Avigad, Cameron E. Freer, Daniel M. Roy, Jason M. Rute
Algorithmic barriers to representing conditional independence. LICS (2019)
Nathanael L. Ackerman, Jeremy Avigad, Cameron E. Freer, Daniel M. Roy, Jason M. Rute
On the computability of graphons. CoRR (2018)
Jeremy Avigad, Jasmin Christian Blanchette, Gerwin Klein, Lawrence C. Paulson, Andrei Popescu, Gregor Snelting
Introduction to Milestones in Interactive Theorem Proving. J. Autom. Reason. 61 (1-4) (2018)
Jeremy Avigad, Assia Mahboubi
Erratum to: Interactive Theorem Proving. ITP (2018)
Jeremy Avigad, Johannes Hölzl, Luke Serafin
A Formally Verified Proof of the Central Limit Theorem. J. Autom. Reason. 59 (4) (2017)
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura
A metaprogramming framework for formal verification. Proc. ACM Program. Lang. 1 (ICFP) (2017)
Jeremy Avigad, Robert Y. Lewis, Cody Roux
A Heuristic Prover for Real Inequalities. J. Autom. Reason. 56 (3) (2016)
Jeremy Avigad, Rebecca Lea Morris
Character and Object. Rev. Symb. Log. 9 (3) (2016)
Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer
The Lean Theorem Prover (System Description). CADE (2015)
Leonardo Mendonça de Moura, Jeremy Avigad, Soonho Kong, Cody Roux
Elaboration in Dependent Type Theory. CoRR (2015)
Jeremy Avigad, Krzysztof Kapulkin, Peter LeFanu Lumsdaine
Homotopy limits in type theory. Math. Struct. Comput. Sci. 25 (5) (2015)
Jeremy Avigad
Thomas Hales. Dense Sphere Packings: A Blueprint for Formal Proofs. Cambridge University Press, Cambridge, 2012, xiv + 271 pp. Bull. Symb. Log. 20 (4) (2014)
Jeremy Avigad, Robert Y. Lewis, Cody Roux
A Heuristic Prover for Real Inequalities. ITP (2014)
Jeremy Avigad, Johannes Hölzl, Luke Serafin
A formally verified proof of the Central Limit Theorem. CoRR (2014)
Jeremy Avigad, John Harrison
Formally verified mathematics. Commun. ACM 57 (4) (2014)
Jeremy Avigad, Robert Y. Lewis, Cody Roux
A heuristic prover for real inequalities. CoRR (2014)
Jeremy Avigad
Uniform distribution and algorithmic randomness. J. Symb. Log. 78 (1) (2013)
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
A Machine-Checked Proof of the Odd Order Theorem. ITP (2013)
Jeremy Avigad, Krzysztof Kapulkin, Peter LeFanu Lumsdaine
Homotopy limits in Coq CoRR (2013)
Sicun Gao, Jeremy Avigad, Edmund M. Clarke
Delta-Decidability over the Reals CoRR (2012)
Jeremy Avigad
Type Inference in Mathematics. Bull. EATCS 106 (2012)
Jeremy Avigad
Uncomputably Noisy Ergodic Limits. Notre Dame J. Formal Log. 53 (3) (2012)
Jeremy Avigad, Edward T. Dean, Jason M. Rute
Algorithmic randomness, reverse mathematics, and the dominated convergence theorem. Ann. Pure Appl. Log. 163 (12) (2012)
Jeremy Avigad, Edward T. Dean, Jason M. Rute
A metastable dominated convergence theorem. J. Log. Anal. 4 (2012)
Sicun Gao, Jeremy Avigad, Edmund M. Clarke
Delta-Complete Decision Procedures for Satisfiability over the Reals CoRR (2012)
Sicun Gao, Jeremy Avigad, Edmund M. Clarke
Delta-Decidability over the Reals. LICS (2012)
Jeremy Avigad, Vasco Brattka
Computability and analysis: the legacy of Alan Turing CoRR (2012)
Jeremy Avigad, Stefan Hetzl
Bondy's Theorem. Arch. Formal Proofs 2012 (2012)
Sicun Gao, Jeremy Avigad, Edmund M. Clarke
δ-Complete Decision Procedures for Satisfiability over the Reals. IJCAR (2012)
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
Building a push-button RESOLVE verifier: Progress and challenges. Formal Aspects Comput. 23 (5) (2011)
Jeremy Avigad
Type inference in mathematics CoRR (2011)
Andrea Asperti, Jeremy Avigad
Zen and the art of formalisation. Math. Struct. Comput. Sci. 21 (4) (2011)
Jeremy Avigad
, John Harrison, Cambridge University Press, 2009. Hardcover, ISBN-13: 978-0-521-89957-4, 681 pp. + xix, $135.00. Theory Pract. Log. Program. 10 (2) (2010)
Jeremy Avigad
The metamathematics of ergodic theory. Ann. Pure Appl. Log. 157 (2-3) (2009)
Jeremy Avigad, Henry Towsner
Functional interpretation and inductive definitions. J. Symb. Log. 74 (4) (2009)
Jeremy Avigad, Edward T. Dean, John Mumma
A Formal System for Euclid's Elements. Rev. Symb. Log. 2 (4) (2009)
Steven Kieffer, Jeremy Avigad, Harvey Friedman
A language for mathematical language management CoRR (2008)
Jeremy Avigad, Yimu Yin
Quantifier elimination for the reals with a predicate for the powers of two. Theor. Comput. Sci. 370 (1-3) (2007)
Jeremy Avigad, Kevin Donnelly
A decision procedure for linear "big O" equations CoRR (2007)
Jeremy Avigad, Kevin Donnelly
A Decision Procedure for Linear "Big O" Equations. J. Autom. Reason. 38 (4) (2007)
Jeremy Avigad, Kevin Donnelly, David Gray, Paul Raff
A formally verified proof of the prime number theorem. ACM Trans. Comput. Log. 9 (1) (2007)
Jeremy Avigad
Mathematical Method and Proof. Synth. 153 (1) (2006)
Jeremy Avigad, Yimu Yin
Quantifier elimination for the reals with a predicate for the powers of two CoRR (2006)
Jeremy Avigad, Harvey Friedman
Combining decision procedures for the reals CoRR (2006)
Jeremy Avigad, Ksenija Simic
Fundamental notions of analysis in subsystems of second-order arithmetic. Ann. Pure Appl. Log. 139 (1-3) (2006)
Jeremy Avigad, Harvey Friedman
Combining decision procedures for the reals. Log. Methods Comput. Sci. 2 (4) (2006)
Jeremy Avigad, Kevin Donnelly, David Gray, Paul Raff
A formally verified proof of the prime number theorem CoRR (2005)
Arnold Beckmann, Jeremy Avigad, Georg Moser
Preface. Ann. Pure Appl. Log. 136 (1-2) (2005)
Jeremy Avigad
Forcing in proof theory. Bull. Symb. Log. 10 (3) (2004)
Jeremy Avigad, Kevin Donnelly
Formalizing O Notation in Isabelle/HOL. IJCAR (2004)
Jeremy Avigad
Eliminating definitions and Skolem functions in first-order logic. ACM Trans. Comput. Log. 4 (3) (2003)
Jeremy Avigad
Erratum to "Saturated models of universal theories": [Ann. Pure Appl. Logic 118 (2002) 219-234]. Ann. Pure Appl. Log. 121 (2-3) (2003)
Jeremy Avigad
Update Procedures and the 1-Consistency of Arithmetic. Math. Log. Q. 48 (1) (2002)
Jeremy Avigad, Jeremy Helzner
Transfer principles in nonstandard intuitionistic arithmetic. Arch. Math. Log. 41 (6) (2002)
Jeremy Avigad
Saturated models of universal theories. Ann. Pure Appl. Log. 118 (3) (2002)
Jeremy Avigad
An Ordinal Analysis of Admissible Set Theory using Recursion on Ordinal Notations. J. Math. Log. 2 (1) (2002)
Jeremy Avigad
Review of "Basic proof theory: second edition" by A. S. Troelstra and H. Schwichtenberg. Cambridge University Press. SIGACT News 32 (2) (2001)
Jeremy Avigad
Algebraic proofs of cut elimination. J. Log. Algebraic Methods Program. 49 (1-2) (2001)
Jeremy Avigad
Eliminating Definitions and Skolem Functions in First-Order Logic. LICS (2001)
Jeremy Avigad
Interpreting Classical Theories in Constructive Ones. J. Symb. Log. 65 (4) (2000)
Jeremy Avigad, Richard Sommer
The Model-Theoretic Ordinal Analysis of Theories of Predicative Strength. J. Symb. Log. 64 (1) (1999)
Jeremy Avigad
. Ann. Pure Appl. Log. 92 (1) (1998)
Jeremy Avigad
An effective proof that open sets are Ramsey. Arch. Math. Log. 37 (4) (1998)
Jeremy Avigad, Richard Sommer
A model-theoretic approach to ordinal analysis. Bull. Symb. Log. 3 (1) (1997)
Jeremy Avigad
. J. Symb. Log. 61 (3) (1996)
Jeremy Avigad
Plausibly hard combinatorial tautologies. Proof Complexity and Feasible Arithmetics (1996)
Jeremy Avigad
Formalizing Forcing Arguments in Subsystems of Second-Order Arithmetic. Ann. Pure Appl. Log. 82 (2) (1996)