Students

I was Director of Graduate Studies in Philosophy at Carnegie Mellon from 2005 to 2009 and again from 2011 to 2012.

PhD students

James Gallicchio (Computer Science, co-advised with Marijn Heule, current)
Chase Norman (Computer Science, current)
Cayden Codel (Computer Science, co-advised with Marijn Heule, current)
MS Thesis: Verifying SAT encodings in Lean.
Hannah Fechtner (Logic, Computation, and Methodology, current)
Joshua Clune (Computer Science, current)
Wojciech Nawrocki (Logic, Computation, and Methodology, current)
MS Thesis: User interfaces for computer-assisted mathematics
Mario Carneiro (PhD Pure and Applied Logic, August 2022)
MS Thesis: The type theory of Lean
PhD Thesis: Metamath Zero: From logic, to proof assistant, to verified computation
Current position: Postdoctoral Fellow, Hoskinson Center for Formal Mathematics
Floris van Doorn (PhD Pure and Applied Logic, May 2018)
PhD Thesis: On the formalization of higher inductive types and synthetic homotopy theory
First positions: Postdoc, Department of Mathematics, University of Pittsburgh, and Postdoc, Laboratoire de Mathématiques d'Orsay (LMO), Université Paris-Saclay
Current position: Professor, Mathematical Institute of the University of Bonn
Robert Lewis (PhD Pure and Applied Logic, May 2018)
PhD Thesis: Two tools for formalizing mathematical proofs
First position: Postdoc, Department of Theoretical Computer Science, Vrije Universiteit Amsterdam
Current position: Lecturer, Department of Computer Science, Brown University
Rebecca Morris (PhD Logic, Computation, and Methodology, August 2015)
PhD Thesis: Appropriate steps: a theory of motivated proof, pdf.
MS thesis: Character and object, pdf.
First positions: Instructor, Department of Philosophy, Carnegie Mellon, and Postdoctoral Fellow, Department of Philosophy, Stanford University.
Jason Rute (PhD Mathematical Sciences, August 2013)
PhD thesis: Topics in algorithmic randomness and computable analysis, pdf.
First positions: Assistant Professor, Department of Mathematics, Pennsylvania State University, and programmer, CiBO Technologies.
Current position: Postdoctoral Researcher in Mathematics of AI at IBM.
Sicun Gao (PhD Logic, Computation, and Methodology, December 2012, co-advised with Ed Clarke)
PhD thesis: Computable analysis, decision procedures, and hybrid automata: a new framework for the formal verification of cyber-physical systems
MS thesis: Counting zeros over finite fields with Gröbner bases.
First positions: Postdoctoral Researcher, Department of Computer Science, Carnegie Mellon University, and Postdoctoral Researcher, Computer Science and Artificial Intelligence Laboratory, MIT
Current position: Assocaite Professor, Department of Computer Science and Engineering, University of California at San Diego
Yimu Yin (PhD Logic, Computation, and Methodology, August 2008)
PhD thesis: Sets, models, and valued fields, pdf.
MS thesis: Quantifier elimination and real closed ordered fields with a predicate for the powers of two, pdf.
First positions: Assistant Professor, Department of Mathematics, University of Pittsburgh; postdoc, École Normale Supérieure; Sun Yat Sen University.
Henry Towsner (PhD Mathematical Sciences, June 2008)
Thesis: Some results in logic and ergodic theory, pdf.
First position: Assistant Professor, Department of Mathematics, University of California, Los Angeles; and participant in the MSRI program in Ergodic Theory and Additive Combinatorics.
Current position: Associate Professor, Department of Mathematics, University of Pennsylvania
Kerry Ojakian (PhD Mathematical Sciences, June 2004)
Thesis: Combinatorics in bounded arithmetic, pdf.
First positions: Postdoctoral Fellow at Charles University, Prague; Postdoctoral Fellow at the Center for Logic and Computation, Lisbon;
Current position: Associate Professor, Department of Mathematics, Bronx Community College
Ksenija Simic-Muller (PhD Mathematical Sciences, May 2004)
Thesis: Aspects of ergodic theory in subsystems of second-order arithmetic, pdf.
First position: Postdoctoral Fellow, Department of Mathematics, University of Arizona.
Current position: Professor, Department of Mathematics, Pacific Lutheran University, Tacoma.

MS students

Paula Neeley (MS Logic, Computation, and Methodology, December 2020)
Thesis: A formalization of dynamic epistemic logic, pdf.
Andrew Warren (MS, Mathematical Sciences, 2019)
Thesis: Fluctuation bounds for ergodic averages of amenable groups on uniformly convex Banach spaces, arXiv. Article version: arXiv.
Seulkee Baek (MS Logic, Computation, and Methodology, 2017)
Thesis: Reflected decision procedures in Lean
Minchao Wu (MS Logic, Computation, and Methodology, August 2017)
Thesis: A formally verified proof of Kruskal's tree theorem in Lean, pdf.
Sebastian Ullrich (Masters' degree from Karlsruhe Institute of Technology, fall 2016; visited Carnegie Mellon under the InterACT program)
Thesis: Simple verification of Rust programs via functional purification, pdf
Project page: github.
Andrew Zipperer (MS Logic, Computation, and Methodology, August, 2016)
Thesis: A formalization of elementary group theory in the proof assistant Lean, pdf.
Luke Serafin (MS Mathematical Sciences, December 2015)
Thesis: A formally verified proof of the central limit theorem, pdf.
Jakob von Raumer (Masters' degree from Karlsruhe Institute of Technology, summer 2015; visited Carnegie Mellon under the InterACT program)
Thesis: Formalization of non-abelian topology for homotopy type theory, pdf.
Code: github.
Benjamin Northrop (MS Logic, Computation, and Methodology, May, 2011)
Thesis: Automated diagrammatic reasoning: a proof checker for the language of E, pdf.
Web page and code: html.
Spencer Breiner (MS Logic, Computation, and Methodology, May, 2010)
Thesis: Towards a practical understanding of mathematical structuralism.
Ed Dean (MS Logic, Computation, and Methodology, August, 2008)
Thesis: In defense of Euclidean proof, pdf.
Steve Kieffer (MS Logic, Computation, and Methodology, August, 2007)
Thesis: A Language for Mathematical Knowledge Management, pdf (and a Powerpoint presentation)
Aaron Hertz (undergraduate honors MS program, Mathematical Sciences, May 2004)
Thesis: A constructive version of the Hilbert basis theorem, pdf.
Doug White (MS Logic, Computation, and Methodology, May 2004)
Thesis: Axiomatics, methodology, and Dedekind's theory of ideals, pdf.
Jessi Berkelhammer (MS Logic, Computation, and Methodology, September 2003)
Thesis: From reducibility to extensionality: the two editions of Principia Mathematica, pdf.
Erica (Lucast) Stonestreet (MS Logic, Computation, and Methodology, December 2002)
Thesis: Proof as method: a new case for proof in mathematics curricula, pdf.

Undergraduate projects supervised

Alex Gillon (BS in Logic and Computation, May 2024)
Senior project: Verified AVL Trees in Lean 4.
Code: github
Minsung Cho (BS in Logic and Computation, May 2022)
Senior project: The Cops and Robber Game in Lean
Ashley Watt (BS in Logic and Computation, May 2019)
Senior project: Treaps in Lean.
Kelvin Rojas (BS in Logic and Computation, May 2015)
Senior project: EuclidZ3 — a Computational Proof-Checker for the Language E, pdf.
Code: github.
Erin Korber (BS in Logic and Computation, May 2005)
Senior project: Implementing decision procedures for the real numbers

Postdocs supervised

Tomáš Skřivan, 2022-present
Mario Carneiro, 2022-present
Ali Mohammed Nezhad, 2022-2023
Edward Ayers, 2022
Gabriel Ebner, 2021-2022
Bruno Bentzen, 2019-2020
Simon Hudon, 2019-2020
Johannes Hölzl, 2017
Cody Roux, 2012-2014
Philipp Gerhardy, 2006-2007

PhD committees

I have served on the following PhD committees, in Philosophy and at Carnegie Mellon, unless otherwise noted:

Jure Taslak (Computer Science, University of Ljubljana, current)
Stephen Mackereth (University of Pittburgh, current)
André Hernández-Espiet (Mathematics, Rutgers, 2024)
Katherine Kosaian (Computer Science, 2023)
Soonho Kong (Computer Science, 2023)
Jesse Han (Mathematics, University of Pittburgh, 2022)
Oskar Abrahamsson (Computer Science and Engineering, Chalmers University of Technology and University of Gothenberg, 2022),
Yong Kiam Tan (Computer Science, 2022)
Andrew Warren (2022)
Jonathan Sterling (Computer Science, 2021)
Edward Ayers (Mathematics, Cambridge University, 2021)
Marcos Mazari (Mathematics, 2021)
Gabriel Ebner, (Computer Science, TU Vienna, 2020)
Carlo Angiuli (Computer Science, 2019)
Nathan Fulton (Computer Science, 2018)
Joseph Tassarotti (Computer Science, 2018)
Egbert Riejke (Pure and Applied Logic, 2018)
Andrew Zucker (Mathematics, 2018)
Mate Szabo (2017)
Sebastian Vasey (Mathematics, 2017)
Kuen-Bang Hou (Favonia) (Computer Science, 2017)
Yacin Hamami (Philosophy, Free University Brussels, 2016)
William Gunther (Mathematics, 2015)
Tyke Nunez (University of Pittsburgh, 2015)
Krzysztof Kapulkin (University of Pittsburgh, Mathematics, 2014)
Spencer Breiner (2014)
Shawn Standefer (University of Pittsburgh, 2013)
Cyril Cohen (Ecole Polytechnique, Computer Science, 2012)
Alexey Solovyev (University of Pittsburgh, Mathematics, 2012)
Ashwini Aroskar (Mathematical Sciences, 2012)
Alexander Kreuzer (Mathematics, TU Munich, 2012)
Matthew Szudzik (Mathematical Sciences, 2010)
Jesse Alama (Stanford, 2009)
Chetan Balwe (Mathematics, University of Pittsburgh, 2008)
Amine Chaieb (Computer Science, TU Munich, 2008)
Henrik Forssell (2007)
Jeremy Heis (Philosophy, University of Pittsburgh, 2007)
Kaustuv Chaudhuri (Computer Science, 2006)
Jyotsna Diwakdar (Mathematics, University of Pittsburgh, 2006)
John Mumma (2006)
Dirk Schlimm (2005)
Mark Ravaglia (2003)
John Krueger (Mathematical Sciences, 2003)
Jesse Hughes (2001)
Barbara Kauffmann (2000)
Alberto Momigliano (2000)
John Byrnes (1999)

MS committees

I have served on the following MS committees, in Philosophy unless otherwise noted:

Connor Gordon (Mathematical Sciences, 2024)
Tomaz Mascarenhas (Computer Science, Universidade Federal de Minas Gerais, 2023)
David Vitali (2020)
William Nalls (2017)
Evan Cavallo (Mathematical Sciences, 2015)
David Carper (2011)
Hans-Christoph Kotzsch (2011)
Brian Leary (Mathematical Sciences, 2009)
Nicholas Radcliffe (2008)
Dave Gilbert (2008)
Kohei Kishida (2007)
George Schaeffer (Mathematical Sciences, 2007)
Lindsay Spriggs (2007)
Michael Warren (2004)
Adam Kramer (2004)
Keith Douglas (2004)
Charlie Smart (Mathematical Sciences, 2002)
John Mumma (2001)
Jeffrey Helzner (2001)
Johanna Franklin (Mathematical Sciences, 2001)
Jay Kim (1999)
Nathaniel Segerlind (Mathematical Sciences, 1998)
Mark Ravaglia (1997)
Chris Skalka (1997)

Logic and Computation majors

I was the director of the Department of Philosophy's major in Logic and Computation from 1997 to 2005. Here is a list of students who graduated during that period of time, with the titles of their senior theses and their advisors:

Sean Hammond, Peirce and the Logic of Science (Teddy Seidenfeld), 2005
Erin Korber, Implementing Decision Procedures for the Real Numbers (Jeremy Avigad), 2005
Lindsay Spriggs, Application of Logic to Computer Security (Benoit Morel), 2005
Jonathan Terleski, Determining Music Similarity: A Pragramatic Approach (Brigham Anderson), 2005
Matt Danish, Compiler Development Aided by Code Certification Techniques (Peter Lee), 2004
William Drozd, Temporal Logic Based Planning for Large-Scale Search and Rescue Operations (Manuela Veloso), 2004
Ryan Eberhard, The Pedagogical Value of Database Theory to Logic Educators (Helen Thomas), 2004
Matthew Hockenberry, Reforming the Ancient Citizen: The Synthesis of Distributed and Deliberative Democracies (Robert Cavalier), 2004
William Lao, Simplifying Data Representations for Temporal Databases in Two Dimensions (Christopher Olston), 2004
William Raul Salinas, Determining Collusion in Negotiations (Teddy Seidenfeld), 2004
Lee Salzman, Prototypes with Multiple Dispatch (Jonathan Aldrich), 2004
Quinten Steenhuis, The Deliberative Opinion Poll: Promises and Challenges (Robert Cavalier), 2004
Eric Castro, Internet Sportsbetting and Incoherence (Teddy Seidenfeld), 2003
Diana Holcomb, Logic and Computation Robot (Wilfried Sieg), 2003.
Charley Price, Evaluation of Interaction Schemes in Computer Role-Playing Games (Don Marinelli), 2003
Avi Silterra, New Semantics for the Simply Typed Lambda Calculus (Steve Awodey), 2003
Michael Strauss, The language of legal statutes and how it affects principles of justice (Martha Harty), 2003
Clinton Field, Automated Proofs of Gödel's Theorems (Wilfried Sieg), 2002
Evan Leonard, A Multi-Perspective Structure for Online Discussion (Susan Fussell), 2002
John Rinderle, Simulation: an open framework for game theoretic simulation (Peter Vanderschraaf), 2002
Andrew Tavares, Optimizing Human Evaluation of Dialogue Translation Systems (Lori Levin), 2002
James Yang, Designing an Adaptive Automotive Control System to Optimize 4-stroke SI Engine Performance (Clark Glymour), 2002
Charles Ballowe, Fully Anonymous Data Sharing (Gregory Kesden), 2001
John Corwin, Linear Logic Theorem Proving Using Artificial Intelligence Planners (Frank Pfenning), 2001
Adam Kramer, Modeling Human Choice (Kevin Kelly), 2001
Stephen Opalenski, An Intuitionistic S5 (Steve Awodey), 2001
Polina Vanyukov, Metaphor: Definition, Interpretation, and Creation (Mandy Simons), 2001
Jonathan Coleman, Musical Style Classification Through Machine Learning (Roger Dannenberg), 2000
John Gasper, Web agents: learning the right strategy (Cristina Bicchieri and Horacio Arlo-Costa), 2000
Laurel Margulis, Who's in Charge? An Evaluation of the Experience of Human Emotions (Horacio Arlo-Costa), 2000
Michele Banko, Resolving Sentence Ambiguity though Speech Act Prediction (Lori Levin and Marsal Gavalda), 1999
Bryan Dougherty, A User-Oriented Approach to Wrapper Generation (Steve Minton), 1999
Roland Reagan, Computer Music Generation via Decision Tree Learning (Roger Dannenberg and Manuela Veloso), 1999
Shane Torsell, Improving Goal Seeking Quality and Efficiency through Automated Agent Reconfiguration and Learning: an application of PRODIGY and HAMLET (Jaime Carbonell), 1999
Robert N. M. Watson, Model Checking to Verify Computer Security Policies (Ed Clarke), 1999
David Wingrove, Borg Concurrency Protocol (Han Kiliccote), 1999
Douglas (Fox) Harrell, Interactive Cinema: Towards a Model of 3rd Person Navigable Story Spaces (Kathleen Newman), 1998
Grant Olds, Application and Testing of Student Modeling in the FIPSE Project (Richard Scheines), 1998

Other

The following students worked on a formalization of the Prime Number Theorem with me:

David Gray (PhD, Philosophy, Carnegie Mellon, 2011)
Kevin Donnelly (MA, Computer Science, Boston University, 2008; now at Google)
Paul Raff (PhD, Mathematics, Rutgers, 2009; then Amazon, and now at Microsoft)
Adam D. I. Kramer (PhD, Psychology, University of Oregon; now at Facebook)