Jeremy Avigad

Jeremy Avigad: Uniform distribution and algorithmic randomness. J. Symb. Log. 78(1): 334-344 (2013)

Jeremy Avigad, Krzysztof Kapulkin, Peter LeFanu Lumsdaine: Homotopy limits in Coq. CoRR abs/1304.0680 (2013)

Jeremy Avigad, Stefan Hetzl: Bondy's Theorem. Archive of Formal Proofs 2012 (2012)

Jeremy Avigad: Uncomputably Noisy Ergodic Limits. Notre Dame Journal of Formal Logic 53(3): 347-350 (2012)

Sicun Gao, Jeremy Avigad, Edmund M. Clarke: δ-Complete Decision Procedures for Satisfiability over the Reals. IJCAR 2012: 286-300

Sicun Gao, Jeremy Avigad, Edmund M. Clarke: Delta-Decidability over the Reals. LICS 2012: 305-314

Sicun Gao, Jeremy Avigad, Edmund M. Clarke: Delta-Complete Decision Procedures for Satisfiability over the Reals. CoRR abs/1204.3513 (2012)

Sicun Gao, Jeremy Avigad, Edmund M. Clarke: Delta-Decidability over the Reals. CoRR abs/1204.6671 (2012)

Jeremy Avigad, Vasco Brattka: Computability and analysis: the legacy of Alan Turing. CoRR abs/1206.3431 (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 Asp. Comput. 23(5): 607-626 (2011)

Andrea Asperti, Jeremy Avigad: Zen and the art of formalisation. Mathematical Structures in Computer Science 21(4): 679-682 (2011)

Jeremy Avigad: Type inference in mathematics. CoRR abs/1111.5885 (2011)

Jeremy Avigad: Handbook of Practical Logic and Automated Reasoning, John Harrison, Cambridge University Press, 2009. Hardcover, ISBN-13: 978-0-521-89957-4, 681 pp. + xix, $135.00. TPLP 10(2): 237-241 (2010)

Jeremy Avigad: The metamathematics of ergodic theory. Ann. Pure Appl. Logic 157(2-3): 64-76 (2009)

Jeremy Avigad, Henry Towsner: Functional interpretation and inductive definitions. J. Symb. Log. 74(4): 1100-1120 (2009)

Steven Kieffer, Jeremy Avigad, Harvey Friedman: A language for mathematical language management. CoRR abs/0805.1386 (2008)

Jeremy Avigad, Kevin Donnelly: A Decision Procedure for Linear "Big O" Equations. J. Autom. Reasoning 38(4): 353-373 (2007)

Jeremy Avigad, Yimu Yin: Quantifier elimination for the reals with a predicate for the powers of two. Theor. Comput. Sci. 370(1-3): 48-59 (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, Kevin Donnelly: A decision procedure for linear "big O" equations. CoRR abs/cs/0701073 (2007)

Jeremy Avigad, Ksenija Simic: Fundamental notions of analysis in subsystems of second-order arithmetic. Ann. Pure Appl. Logic 139(1-3): 138-184 (2006)

Jeremy Avigad, Harvey Friedman: Combining decision procedures for the reals. Logical Methods in Computer Science 2(4) (2006)

Jeremy Avigad: Mathematical Method and Proof. Synthese 153(1): 105-159 (2006)

Jeremy Avigad, Harvey Friedman: Combining decision procedures for the reals. CoRR abs/cs/0601134 (2006)

Jeremy Avigad, Yimu Yin: Quantifier elimination for the reals with a predicate for the powers of two. CoRR abs/cs/0610117 (2006)

Arnold Beckmann, Jeremy Avigad, Georg Moser: Preface. Ann. Pure Appl. Logic 136(1-2): 1-2 (2005)

Jeremy Avigad, Kevin Donnelly, David Gray, Paul Raff: A formally verified proof of the prime number theorem. CoRR abs/cs/0509025 (2005)

Jeremy Avigad: Forcing in proof theory. Bulletin of Symbolic Logic 10(3): 305-333 (2004)

Jeremy Avigad, Kevin Donnelly: Formalizing O Notation in Isabelle/HOL. IJCAR 2004: 357-371

Jeremy Avigad: Erratum to "Saturated models of universal theories": [Ann. Pure Appl. Logic 118 (2002) 219-234]. Ann. Pure Appl. Logic 121(2-3): 285- (2003)

Jeremy Avigad: Eliminating definitions and Skolem functions in first-order logic. ACM Trans. Comput. Log. 4(3): 402-415 (2003)

Jeremy Avigad: Saturated models of universal theories. Ann. Pure Appl. Logic 118(3): 219-234 (2002)

Jeremy Avigad: Update Procedures and the 1-Consistency of Arithmetic. Math. Log. Q. 48(1): 3-13 (2002)

Jeremy Avigad: Algebraic proofs of cut elimination. J. Log. Algebr. Program. 49(1-2): 15-30 (2001)

Jeremy Avigad: Review of "Basic proof theory: second edition" by A. S. Troelstra and H. Schwichtenberg. Cambridge University Press. SIGACT News 32(2): 15-19 (2001)

Jeremy Avigad: Eliminating Definitions and Skolem Functions in First-Order Logic. LICS 2001: 139-146

Jeremy Avigad: Interpreting Classical Theories in Constructive Ones. J. Symb. Log. 65(4): 1785-1812 (2000)

Jeremy Avigad, Richard Sommer: The Model-Theoretic Ordinal Analysis of Theories of Predicative Strength. J. Symb. Log. 64(1): 327-349 (1999)

Jeremy Avigad: An effective proof that open sets are Ramsey. Arch. Math. Log. 37(4): 235-240 (1998)

Jeremy Avigad: Predicative Functionals and an Interpretation of ID_<omega. Ann. Pure Appl. Logic 92(1): 1-34 (1998)

Jeremy Avigad, Richard Sommer: A model-theoretic approach to ordinal analysis. Bulletin of Symbolic Logic 3(1): 17-52 (1997)

Jeremy Avigad: Formalizing Forcing Arguments in Subsystems of Second-Order Arithmetic. Ann. Pure Appl. Logic 82(2): 165-191 (1996)

Jeremy Avigad: On the Relationship Between ATR₀ and ID_<omega. J. Symb. Log. 61(3): 768-779 (1996)