 | 2011 |
| 34 |  | Jeremy Avigad:
Type inference in mathematics
CoRR abs/1111.5885: (2011) |
| 33 |  | 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) |
| 32 |  | Andrea Asperti,
Jeremy Avigad:
Zen and the art of formalisation.
Mathematical Structures in Computer Science 21(4): 679-682 (2011) |
| 2010 |
| 31 |  | 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) |
| 2009 |
| 30 |  | Jeremy Avigad:
The metamathematics of ergodic theory.
Ann. Pure Appl. Logic 157(2-3): 64-76 (2009) |
| 29 |  | Jeremy Avigad,
Henry Towsner:
Functional interpretation and inductive definitions.
J. Symb. Log. 74(4): 1100-1120 (2009) |
| 2008 |
| 28 |  | Steven Kieffer,
Jeremy Avigad,
Harvey Friedman:
A language for mathematical language management
CoRR abs/0805.1386: (2008) |
| 2007 |
| 27 |  | Jeremy Avigad,
Kevin Donnelly,
David Gray,
Paul Raff:
A formally verified proof of the prime number theorem.
ACM Trans. Comput. Log. 9(1): (2007) |
| 26 |  | Jeremy Avigad,
Kevin Donnelly:
A decision procedure for linear "big O" equations
CoRR abs/cs/0701073: (2007) |
| 25 |  | Jeremy Avigad,
Kevin Donnelly:
A Decision Procedure for Linear "Big O" Equations.
J. Autom. Reasoning 38(4): 353-373 (2007) |
| 24 |  | 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) |
| 2006 |
| 23 |  | Jeremy Avigad,
Ksenija Simic:
Fundamental notions of analysis in subsystems of second-order arithmetic.
Ann. Pure Appl. Logic 139(1-3): 138-184 (2006) |
| 22 |  | Jeremy Avigad,
Harvey Friedman:
Combining decision procedures for the reals
CoRR abs/cs/0601134: (2006) |
| 21 |  | Jeremy Avigad,
Yimu Yin:
Quantifier elimination for the reals with a predicate for the powers of two
CoRR abs/cs/0610117: (2006) |
| 20 |  | Jeremy Avigad,
Harvey Friedman:
Combining decision procedures for the reals.
Logical Methods in Computer Science 2(4): (2006) |
| 19 |  | Jeremy Avigad:
Mathematical Method and Proof.
Synthese 153(1): 105-159 (2006) |
| 2005 |
| 18 |  | Arnold Beckmann,
Jeremy Avigad,
Georg Moser:
Preface.
Ann. Pure Appl. Logic 136(1-2): 1-2 (2005) |
| 17 |  | Jeremy Avigad,
Kevin Donnelly,
David Gray,
Paul Raff:
A formally verified proof of the prime number theorem
CoRR abs/cs/0509025: (2005) |
| 2004 |
| 16 |  | Jeremy Avigad,
Kevin Donnelly:
Formalizing O Notation in Isabelle/HOL.
IJCAR 2004: 357-371 |
| 15 |  | Jeremy Avigad:
Forcing in proof theory.
Bulletin of Symbolic Logic 10(3): 305-333 (2004) |
| 2003 |
| 14 |  | Jeremy Avigad:
Eliminating definitions and Skolem functions in first-order logic.
ACM Trans. Comput. Log. 4(3): 402-415 (2003) |
| 13 |  | 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) |
| 2002 |
| 12 |  | Jeremy Avigad:
Saturated models of universal theories.
Ann. Pure Appl. Logic 118(3): 219-234 (2002) |
| 11 |  | Jeremy Avigad:
Update Procedures and the 1-Consistency of Arithmetic.
Math. Log. Q. 48(1): 3-13 (2002) |
| 2001 |
| 10 |  | Jeremy Avigad:
Eliminating Definitions and Skolem Functions in First-Order Logic.
LICS 2001: 139-146 |
| 9 |  | Jeremy Avigad:
Algebraic proofs of cut elimination.
J. Log. Algebr. Program. 49(1-2): 15-30 (2001) |
| 8 |  | 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) |
| 2000 |
| 7 |  | Jeremy Avigad:
Interpreting Classical Theories in Constructive Ones.
J. Symb. Log. 65(4): 1785-1812 (2000) |
| 1999 |
| 6 |  | Jeremy Avigad,
Richard Sommer:
The Model-Theoretic Ordinal Analysis of Theories of Predicative Strength.
J. Symb. Log. 64(1): 327-349 (1999) |
| 1998 |
| 5 |  | Jeremy Avigad:
Predicative Functionals and an Interpretation of ID<omega.
Ann. Pure Appl. Logic 92(1): 1-34 (1998) |
| 4 |  | Jeremy Avigad:
An effective proof that open sets are Ramsey.
Arch. Math. Log. 37(4): 235-240 (1998) |
| 1997 |
| 3 |  | Jeremy Avigad,
Richard Sommer:
A model-theoretic approach to ordinal analysis.
Bulletin of Symbolic Logic 3(1): 17-52 (1997) |
| 1996 |
| 2 |  | Jeremy Avigad:
Formalizing Forcing Arguments in Subsystems of Second-Order Arithmetic.
Ann. Pure Appl. Logic 82(2): 165-191 (1996) |
| 1 |  | Jeremy Avigad:
On the Relationship Between ATR0 and ID<omega.
J. Symb. Log. 61(3): 768-779 (1996) |