Publications

This list includes resarch articles, surveys, expository articles, unpublished notes, and a translation. I have also done work in formally verified mathematics using the Isabelle proof assistant.

• A language for mathematical knowledge management
  with Steven Kieffer and Harvey Friedman, Carnegie Mellon Technical Report CMU-PHIL-181, 2008
  Paper: arXiv. Associated materials: html.
   
• The metamathematics of ergodic theory
  to appear in the Annals of Pure and Applied Logic
  Paper: pdf.
   
• Functional interpretation and inductive definitions
  with Henry Towsner, submitted.
  Paper: arXiv
   
• Local stability of ergodic averages
  with Philipp Gerhardy and Henry Towsner, to appear in Transactions of the American Mathematical Society.
  Paper: arXiv
   
• Response to questionnaire
  in Vincent F. Hendricks and Hannes Leitgeb, editors, Philosophy of Mathematics: 5 questions, Automatic / VIP Press, 2007
  Book site: html, Paper: pdf (letter), pdf (a4)
   
• A decision procedure for linear "big O" equations
  with Kevin Donnelly, Journal of Automated Reasoning 38: 353-373, 2007
  Abstract: html, Paper: journal, arXiv, Implementation: sml
   
• A variant of the double-negation translation
  Carnegie Mellon Technical Report CMU-PHIL 179
  Abstract: html, Paper: pdf (letter), pdf (a4)
   
• Gödel and the metamathematical tradition
  to appear in a collection essays published in the ASL Lecture Notes in Logic series
  Paper: pdf (letter), pdf (a4).
   
• Understanding proofs
  to appear in Paolo Mancosu, editor, The Philosophy of Mathematical Practice, Oxford University Press
  Paper: pdf (letter), pdf (a4).
   
• Computers in mathematical inquiry
  to appear in Paolo Mancosu, editor, The Philosophy of Mathematical Practice, Oxford University Press
  Paper: pdf (letter), pdf (a4).
   
• Combining decision procedures for the reals
  with Harvey Friedman, Logical Methods in Computer Science, 2(4:4):1-42, 2006
  Paper: journal, arXiv
   
• A formally verified proof of the prime number theorem
  with Kevin Donnelly, David Gray, and Paul Raff, ACM Transactions on Computational Logic, 9(1:2):1-23, 2007
  Paper: journal, arXiv
   
• Quantifier elimination for the reals with a predicate for the powers of two
  with Yimu Yin, Theoretical Computer Science, 370:48-59, 2007
  Paper: journal, arXiv
   
• Methodology and metaphysics in the development of Dedekind's theory of ideals
  in José Ferreirós and Jeremy Gray, editors, The Architecture of Modern Mathematics, Oxford University Press, 159-186, 2006
  Paper: pdf (letter), pdf (a4)
   
• Notes on a formalization of the prime number theorem
  Carnegie Mellon Technical Report CMU-PHIL-163, 2004
  Paper: pdf (letter), pdf (a4)
   
• Philosophy of mathematics
  in Constantin Boundas, editor, The Edinburgh Companion to Twentieth-Century Philosophies, Edinburgh University Press, 2007, also published as The Columbia Companion to Twentieth-Century Philosophies, Columbia University Press, 2007
  Paper: pdf (letter), pdf (a4).
   
• Dedekind's 1871 version of ideal theory
  translation, with an introduction; Carnegie Mellon Technical Report CMU-PHIL-162, 2004
  Paper: pdf (letter), pdf (a4). The original version: pdf.
   
• Mathematical method and proof
  Synthese 153:105-159, 2006
  Abstract: html, Paper: journal, pdf (letter), pdf (a4)
   
• Formalizing O notation in Isabelle/HOL
  with Kevin Donnelly, in David Basin and Michaël Rusinowitch, editors, Automated Reasoning: second international joint conference, IJCAR 2004, Lecture Notes in Artificial Intelligence 3097, Springer, 357-371, 2004
  Abstract: html, Paper: pdf (letter), pdf (a4)
   
• Fundamental notions of analysis in subsystems of second-order arithmetic
  with Ksenija Simic, Annals of Pure and Applied Logic, 139:138-184, 2006
  Abstract: html, Paper: pdf (letter), pdf (a4), published version
   
• Forcing in proof theory
  Bulletin of Symbolic Logic, 10:305-333, 2004
  Abtract: html, Paper: pdf (letter), pdf (a4). Published version: html. Erratum: html.
   
• Eliminating definitions and Skolem functions in first-order logic
  ACM Transactions on Computational Logic, 4:402-415, 2003. (Conference version: Logic in Computer Science 2001, Springer, 139-146.)
  Abstract: html, Paper: portal link, pdf
   
• Weak theories of nonstandard arithmetic and analysis
  in Stephen Simpson, editor, Reverse Mathematics 2001, A K Peters, 19-46, 2005
  Abstract: html, Paper: dvi, postscript, pdf
   
• Notes on Pi^1_1 conservativity, omega-submodels, and the collection schema
  Carnegie Mellon Technical Report CMU-PHIL-125, 2001
  Abtract: html, Paper: dvi, postscript, pdf
   
• Number theory and elementary arithmetic
  Philosophia Mathematica, 11:257-284, 2003
  Abtract: html, Paper: pdf.
   
• Saturated models of universal theories
  Annals of Pure and Applied Logic, 118:219-234, 2002
  Abstract: html, Complaint: html, Paper: dvi, postscript, pdf
   
• Algebraic proofs of cut elimination
  Journal of Logic and Algebraic Programming, 49:15-30, 2001
  Abstract: html, Paper: dvi, postscript, pdf
   
• Update procedures and the 1-consistency of arithmetic
  Mathematical Logic Quarterly, 48:3-13, 2002
  Abstract: html, Paper: dvi, postscript, pdf
   
• The epsilon calculus
  with Richard Zach, in the Stanford Encyclopedia of Philosophy
  Article: html.
   
• "Clarifying the nature of the infinite": the development of metamathematics and proof theory
  with Erich H. Reck, Carnegie Mellon Technical Report CMU-PHIL-120, 2001
  Abtract: html, Paper: dvi, postscript, pdf.
   
• An ordinal analysis of admissible set theory using recursion on ordinal notations
  Journal of Mathematical Logic, 2:91-112, 2002
  Abstract: html, Paper: dvi, postscript, pdf
      
• Transfer principles in nonstandard intuitionistic arithmetic
  with Jeffrey Helzner, Archive for Mathematical Logic, 41:581-602, 2002
  Abstract: html, Paper: dvi, postscript, pdf
   
• Ordinal analysis without proofs
  in W. Sieg et al. eds., Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman, Lecture Notes in Logic 15, ASL Publications, A K Peters, 1-36, 2002
  Abstract: html, Paper: dvi, postscript, pdf
   
• Interpreting classical theories in constructive ones
  Journal of Symbolic Logic, 65:1785-1812, 2000
  Abstract: html, Paper: dvi, postscript, pdf
   
• A realizability interpretation for classical arithmetic
  in Buss, Hájek, and Pudlák eds., Logic Colloquium '98, Lecture Notes in Logic 13, AK Peters, 57-90, 2000
  Abstract: html, Paper: dvi, postscript, pdf
   
• The model-theoretic ordinal analysis of predicative theories
  with Richard Sommer, Journal of Symbolic Logic, 64:327-349, 1999
  Abstract: html, Paper: dvi, postscript, pdf
   
• Gödel's functional ("Dialectica") interpretation
  with Solomon Feferman, in S. Buss ed., The Handbook of Proof Theory, North-Holland, 337-405, 1999
  Abtract: html, Paper: dvi, postscript, pdf.
   
• Plausibly hard combinatorial tautologies
  in Beame and Buss eds., Proof Complexity and Feasible Arithmetics, American Mathematical Society, 1-12, 1997
  Abstract: html, Paper: dvi, postscript, pdf
   
• A model-theoretic approach to ordinal analysis
  with Richard Sommer, Bulletin of Symbolic Logic, 3:17-52, 1997
  Abstract: html, Paper: dvi, postscript, pdf
   
• An effective proof that open sets are Ramsey
  Archive for Mathematical Logic, 37:235-240, 1998
  Abstract: html, Paper: dvi, postscript, pdf
   
• Predicative functionals and an interpretation of ID^_<omega
  Annals of Pure and Applied Logic, 92:1-34, 1998
  Abstract: html, Paper: dvi, postscript, pdf
   
• Formalizing forcing arguments in subsystems of second-order arithmetic
  Annals of Pure and Applied Logic, 82:165-191, 1996
  Abstract: html, Paper: dvi, postscript, pdf
   
• On the relationship between ID^_<omega and ATR_0
  Journal of Symbolic Logic, 61:768-779, 1996
  Abstract: html, Paper: dvi, postscript, pdf