Welcome

Research

Papers

Books

Reviews

Talks

Teaching

Students

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)
  MS Thesis: Braids in Lean
• 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
  First position: Postdoctoral Fellow, Hoskinson Center for Formal Mathematics
  Current position: Postdoctoral Researcher, Computer Science and Engineering, Chalmers University
• 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

• Aeacus Sheng (MS Logic, Computation, and Methodology, current)
  
• Thomas Zhu (MS Language Technologies Institute, co-advised with Sean Welleck, current)
• 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

• Peter Khoudary (BS in Logic and Computation, May 2025)
  Senior project: Provably correct priority queues in Lean, pdf.
• Alex Gillon (BS in Logic and Computation, May 2024)
  Senior project: Verified AVL Trees in Lean 4, pdf.
  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-2025
• Mario Carneiro, 2022-2024
• 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)
• Emre Yolcu (Computer Science, current)
• Albert Jiang (Computer Science, University of Cambridge, 2024)
• Stephen Mackereth (University of Pittsburgh, 2024)
• André Hernández-Espiet (Mathematics, Rutgers, 2024)
• Katherine Kosaian (Computer Science, 2023)
• Soonho Kong (Computer Science, 2023)
• Jesse Han (Mathematics, University of Pittsburgh, 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)