I was Director of Graduate Studies in Philosophy at Carnegie Mellon from 2005 to 2009 and again from 2011 to 2012.
- 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)
- 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
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
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
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.
- 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.
- 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.
- 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 committeesI have served on the following PhD committees, in Philosophy and at Carnegie Mellon, unless otherwise noted:
- Jure Taslak (Computer Science, University of Ljubljana, current)
- Katherine Cordwell (Computer Science, current)
- Stephen Mackereth (University of Pittburgh, current)
- 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 committeesI have served on the following MS committees, in Philosophy unless otherwise noted:
- 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)
Undergraduate studentsI supervised the following undergraduate projects:
- 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.
- Erin Korber (BS in Logic and Computation, May 2005)
Senior project: Implementing decision procedures for the real numbers
- 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
The following students have worked on a formalization of the Prime Number Theorem with me: