Welcome to my home page. I am a professor in the Department of Philosophy and the Department of Mathematical Sciences at Carnegie Mellon University, and associated with Carnegie Mellon's interdisciplinary program in Pure and Applied Logic. You can also read my CV.
Mathematical logic, proof theory, philosophy of mathematics, formal verification, automated reasoning, history of mathematics.
Baker Hall 135E
Department of Philosophy
Baker Hall 161
Carnegie Mellon University
Pittsburgh, PA 15213
I am on the editorial boards of the Journal of Automated Reasoning, Computability, Logical Methods in Computer Science, the Journal of Logic and Analysis, and the Journal of Formalized Reasoning. The last three are open access journals.
Johannes Hölzl, Luke Serafin, and I have written a paper on our formalization of the Central Limit Theorem: pdf, online.
Sebastian Ullrich just completed a master's thesis on program verification: Simple Verification of Rust Programs via Functional Purification, pdf. The project page is here: github.
The Notices of the AMS has just published my review of two books about Gerhard Gentzen.
I have made a draft of new paper, Modularity in mathematics, available: pdf.
I am contributing to the development of a new theorem prover, Lean. There is a tutorial introduction here: online version, pdf.
Rob Lewis, Floris van Doorn, and I have prepared materials based on Lean for an undergraduate course: online version, pdf.
I gave a series of lectures as part of a thematic trimester, "Current Issues in the Philosophy of Practice of Mathematics and Informatics," last summer in Toulouse: html.