Welcome to my home page. I am a professor in the Department of Philosophy at Carnegie Mellon University, and (by courtesy) in the Department of Mathematical Sciences. I am associated with Carnegie Mellon's interdisciplinary program in Pure and Applied Logic. You can read my CV.
Mathematical logic, proof theory, philosophy of mathematics, formal verification, automated reasoning, history of mathematics.
Office: Baker Hall 135E
Department of Philosophy
Baker Hall 161
Carnegie Mellon University
Pittsburgh, PA 15213
I will teach a course on interactive theorem proving in the spring of 2019.
An article I wrote on the relationship between philosophy and mathematics, with some reflection on the state of the philosophy of mathematics today, has appeared in Aeon: html.
I heartily endorse the following slogan, which I learned from Arthur Krener: "Think mathematically, act computationally."
My article on the Mechanization of Mathematics has appeared in the Notices of the AMS. There are slides from an associated talk here: pdf.
I recently organized a workshop, Applications of Formal Methods to Control Theory and Dynamical Systems.
Assia Mahboubi and I were the program committee chairs for Interactive Theorem Proving, part of the Federated Logic Conference this year.
Gerwin Klein, Larry Paulson, and I edited a special issue of the Journal of Automated Reasoning called Milestones in Interactive Theorem Proving. It is dedicated to Tobias Nipkow on the occasion of this 60th birthday. Together with Jasmin Blanchette, Andrei Popescu, and Gregor Snelting, we also wrote an introduction with a short overview of Tobias' career.
Floris van Doorn has successfully defended his PhD thesis: On the formalization of higher inductive types and synthetic homotopy theory, pdf.
Rob Lewis has successfully defended his PhD thesis: Two tools for formalizing mathematical proofs, pdf.
I gave a talk in Calgary in March, Philosophy of Mathematics as a Design Science. You can watch the video.
"Modularity in Mathematics" has been accepted to the Review of Symbolic Logic. Preprint: doi, philsci archive.
I have contributed 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 introduction to logic and mathematical proof: online version, pdf. You can read about the course here: pdf. I also maintain a web page with additional resources for using formal methods in education.
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.