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

- Wojciech Nawrocki (Logic, Computation, and Methodology, current)
- Joshua Clune (Computer Science, current)
- Evan Lohn (Computer Science, current, co-advising with Marijn Heule)
- Seul Baek (Logic, Computation, and Methodology, current)

MS Thesis:*Reflected decision procedures in Lean*, pdf. - Mario Carneiro (Pure and Applied Logic, current)

MS Thesis:*The type theory of Lean*, github. - Floris van Doorn (PhD in Pure and Applied Logic, May 2018)

PhD Thesis:*On the formalization of higher inductive types and synthetic homotopy theory*, pdf.

First position: Postdoc, Department of Mathematics, University of Pittsburgh.

Current position: Postdoc, Laboratoire de Mathématiques d'Orsay (LMO), Université Paris-Saclay. - Robert Lewis (PhD in Pure and Applied Logic, May 2018)

PhD Thesis:*Two tools for formalizing mathematical proofs*, pdf.

First position: Postdoc, Department of Theoretical Computer Science, Vrije Universiteit Amsterdam.

Current position: Lecturer, Department of Computer Science, Brown University. - Rebecca Morris
(PhD in 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, CiBO Technologies.

Current position: Postdoctoral Researcher in Mathematics of AI at IBM. - Sicun Gao (PhD in 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*, pdf.

First positions: Postdoctoral Researcher, Department of Computer Science, Carnegie Mellon University, and Postdoctoral Researcher, Computer Science and Artificial Intelligence Laboratory, MIT.

Current position: Assistant Professor, Department of Computer Science and Engineering, University of California at San Diego. - Yimu
Yin (PhD in 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: Assistant 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: Associate Professor, Department of Mathematics, Pacific Lutheran University, Tacoma.

- Cayden Codel (Computer Science, current; co-advised with Marijn Heule).
Thesis:
*Verifying SAT encodings in Lean*, pdf. - Paula Neeley (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. - 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.

Currently working for the US Department of Defense. - 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.

- 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*

- Ali Mohammed Nezhad, 2022-present
- Edward Ayers, 2022-present
- Gabriel Ebner, 2021-2022
- Bruno Bentzen, 2019-2020
- Simon Hudon, 2019-2020
- Johannes Hölzl, 2017
- Cody Roux, 2012-2014
- Philipp Gerhardy, 2006-2007

The following students have 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)

- Jesse Han (Mathematics, University of Pittburgh, current)
- Katherine Cordwell (Computer Science, current)
- Stephen Mackereth (University of Pittburgh, current)
- Yong Kiam Tan (Computer Science, current)
- Colin Zwanziger (Pure and Applied Logic, current)
- 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)

- Will 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)

- 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