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, current; co-advised with Marijn Heule).
MS Thesis: Verifying SAT encodings in Lean,
- Joshua Clune (Computer Science, current)
- Evan Lohn (Computer Science, current, co-advised with Marijn Heule)
- Wojciech Nawrocki (Logic, Computation, and Methodology, current)
- Seul Baek (Logic, Computation, and Methodology, current)
MS Thesis: Reflected decision procedures in Lean,
- Mario Carneiro (Pure and Applied Logic, August 2022)
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,
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,
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,
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
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.
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.
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
First position: Assistant Professor,
Department of Mathematics, University of California, Los Angeles;
and participant in the MSRI program in Ergodic Theory and Additive
Current position: Associate Professor, Department of Mathematics, University of Pennsylvania
- Kerry Ojakian (PhD Mathematical Sciences, June
Thesis: Combinatorics in bounded arithmetic, pdf.
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.
position: Associate Professor, Department of Mathematics, Pacific Lutheran University,
- Paula Neeley (Logic, Computation, and Methodology, December 2020)
Thesis: A formalization of dynamic epistemic logic,
- 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,
- 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,
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,
- Benjamin Northrop
(MS Logic, Computation, and Methodology, May, 2011)
Thesis: Automated diagrammatic reasoning: a proof checker for the language of E,
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)
Language for Mathematical Knowledge Management, pdf (and a Powerpoint
- 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)
methodology, and Dedekind's theory of ideals, pdf.
- Jessi Berkelhammer (MS Logic, Computation, and Methodology, September 2003)
From reducibility to extensionality: the two editions of
Principia Mathematica, pdf.
Erica (Lucast) Stonestreet (MS Logic, Computation, and Methodology, December 2002)
Proof as method: a new case for proof in mathematics
- 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,
- 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:
I have served on the following PhD committees (in Philosophy and at Carnegie Mellon,
unless otherwise noted):
- David Gray (PhD, Philosophy, Carnegie Mellon, 2011)
Donnelly (MA, Computer Science, Boston University, 2008;
now at Google)
- Paul Raff (PhD, Mathematics, Rutgers, 2009; then Amazon, and now at Microsoft)
D. I. Kramer (PhD, Psychology, University of Oregon; now at Facebook)
I have served on the following MS committees (in Philosophy, unless
- Jesse Han (Mathematics, University of Pittburgh, current)
- Stephen Mackereth (University of Pittburgh, current)
- Oskar Abrahamsson (Chalmers University of Technology and University of Gothenberg, Computer Science and Engineering, 2022),
- Katherine Cordwell (Computer Science, 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)
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:
- 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
(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
- 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
- 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
- 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