Alumni
The following is a list of students who earned a PhD in Computer Science, Mathematical Sciences, or Philosophy, and wrote a
dissertation in a logicrelated area under the supervision of a member of the PAL faculty.
2022
 Mario Carneiro
Thesis: Metamath Zero: From Logic, to Proof Assistant, to Verified Compiler
Department: Philosophy
Advisor: Jeremy Avigad
First position: Postdoctoral Research Fellow, Hoskinson Center, Carnegie Mellon University
 Hanif Cheung
Thesis: Notions of Amalgamation for Abstract Elementary Classes
Department: Mathematical Sciences
Advisor: Rami Grossberg
First position: Morgan Stanley, UK
 Yong Kiam Tan
Thesis: Deductive Verification for Ordinary Differential Equations: Safety, Liveness, and Stability
Department: Computer Science
Advisor: André Platzer
First position: Institute for Infocomm Research, Singapore
2021
 Shaun Allison
Thesis: Actions of Polish groups and anticlassification
results
Department: Mathematical Sciences
Advisor: Clinton Conley
First position: Postdoctoral Fellow, Mathematics, Hebrew University
 Brandon Bohrer
Thesis: Practical EndtoEnd Verification of CyberPhysical Systems
Department: Computer Science
Advisor: André Platzer
First position: Assistant Professor, Worcester Polytechnic Institute
 Farzaneh Derakhshan
Thesis: SessionTyped Recursive Processes and Circular Proofs
Department: Computer Science
Advisor: Frank Pfenning
First position: Postdoctoral Fellow, Cylab, Carnegie Mellon University
 Sittinon Jirattitkansakul
Thesis: Blowing up the power of a singular cardinal of any cofinality with collapses
Department: Mathematical Sciences
Advisor: James Cummings
First position: Postdoctoral Fellow, Mathematics, Tel Aviv University
 Marcos MazariArmida
Thesis: Remarks on classification theory for abstract elementary classes with applications to abelian group theory and ring theory
Department: Mathematical Sciences
Advisor: Rami Grossberg
First position: Burnett Meyer Postoctoral Fellow, Mathematics,
University of Colorado, Boulder
2019
 Patrick Walsh
Thesis: Categorical characterization of accessible domains
Department: Philosophy
Advisor: Wilfried Sieg
First position: Assistant Teaching Professor, CMUQatar
 Jing Zhang
Thesis: Some Results in Combinatorial Set Theory
Department: Mathematical Sciences
Advisor: James Cummings
First position: Israel Academy of Sciences and Humanities Postdoctoral
Fellow, Mathematics, BarIlan University
2018
 Nathan Fulton
Thesis: Verifiably Safe Autonomy for CyberPhysical Systems
Department: Computer Science
Advisor: André Platzer
First position: Researcher, MITIBM Watson AI Lab
 Robert Lewis
Thesis: Two tools for formalizing mathematical proofs
Department: Philosophy
Advisor: Jeremy Avigad
First position: Postdoctoral fellow, Theoretical Computer Science, Vrije Universiteit Amsterdam
 Clive Newstead
Thesis: Algebraic models of dependent type theory
Department: Mathematical Sciences
Advisor: Steve Awodey
First position: Postdoctoral Lecturer, Mathematics Department,
Northwestern University
 Egbert Rijke
Thesis: Classifying types
Department: Philosophy (Pure and Applied Logic)
Advisor: Steve Awodey
First position:
Postdoctoral Researcher, Mathematics Department,
University of Illinois UrbanaChampaign
 Floris van Doorn
Thesis: On the formalization of higher inductive types and synthetic homotopy theory
Department: Philosophy
Advisor: Jeremy Avigad
First position:
Postdoctoral fellow, Department of Mathematics, University of Pittsburgh
 Andy Zucker
Thesis: New directions in the abstract topological dynamics of Polish groups
Department: Mathematical Sciences
Advisor: Clinton Conley
First position:
NSF Mathematical Sciences Postdoctoral Research Fellowship,
Institut de Mathématiques,
Université Paris Diderot, France
Later position: Assistant Professor, Mathematics, University of Waterloo
2017
 Máté Szabó
Thesis: Human and Machine Computation, an Exploration
Department: Philosophy
Advisor: Wilfried Sieg
First position: Postdoctoral Fellow, FFIUM Research Program, Nancy and Paris
 Sebastien Vasey
Thesis: Superstability and Categoricity in Abstract Elementary Classes Department: Mathematical Sciences
Advisor: Rami Grossberg
First position: Benjamin Peirce Fellow, Mathematics, Harvard University
2016
 Jacob Davis
Thesis: Universal graphs at ℵ_{ω1} and settheoretic geology Department: Mathematical Sciences
Advisor: James Cummings
First position: Google Zurich
 Kristina Sojakova
Thesis: Higher Inductive Types as HomotopyInitial Algebras
Department: Computer Science
Advisor: Steve Awodey (Philosophy) and Frank Pfenning
Winner of the 2016 CMU SCS Dissertation Award
 Sarah Loos
Thesis: Differential Refinement Logic
Department: Computer Science
Advisor: André Platzer
First position: Google Research
 Daniel Rodriguez
Thesis: Models of ℝsupercompactness
Department: Mathematical Sciences
Advisor: Ernest Schimmerling
First position: Google Research
2015
 William Gunther
Thesis: Results on classical semantics and polymorphic types
Department: Mathematical Sciences
Advisor: Richard Statman
 Chris Martens
Thesis: Programming Interactive Worlds with Linear Logic
Department: Computer Science
Advisor: Karl Crary and Frank Pfenning
 Rebecca Morris
Thesis: Appropriate steps: a theory of motivated proofs
Department: Philosophy
Advisor: Jeremy Avigad
First position: Instructor, Department of Philosophy, Carnegie Mellon University
 Bernardo Toninho
Thesis: A Logical Foundation for Sessionbased Concurrent
Computation
Department: Computer Science
Advisor: Luis Caires (Universidade Nova de Lisboa) and Frank Pfenning
2014
 Will Boney
Thesis: Advances in classification theory for abstract elementary classes
Department: Mathematical Sciences
Advisor: Rami Grossberg
First positions: NSF Postdoctoral Research Fellowship, Mathematics,
University of Illinois at Chicago; Benjamin Peirce Fellowship, Mathematics,
Harvard University
 Spencer Breiner
Thesis: Scheme representation for firstorder logic
Department: Philosophy
Advisor: Steve Awodey
First position: Postdoctoral Researcher, National Institute of Standards & Technology
 Chris LambieHanson
Thesis: Covering matrices, squares, scales and stationary reflection
Department: Mathematical Sciences
Advisor: James Cummings
First position: Lady Davis Postdoctoral Fellow, Einstein Institute of Mathematics, Hebrew University of Jerusalem
2013
 Paul McKenney
Thesis: Forcing axioms and the rigidity of corona algebras
Department: Mathematical Sciences
Advisor: Ernest Schimmerling
First position: Visiting Assistant Professor, Department of Mathematics, Miami University
 Jason Rute
Thesis: Topics in algorithmic randomness and computable analysis
Department: Mathematical Sciences
Advisor: Jeremy Avigad
First position: Postdoctoral Assistant Professor, Department of Mathematics, Pennsylvania State University
 Spencer Unger
Thesis: Some results on the tree property
Department: Mathematical Sciences
Advisor: James Cummings
First position: RTG Assistant Professor, Department of Mathematics, UCLA
Later position: Assistant Professor, Mathematics, University of Toronto
2012
 Ashwini Aroskar
Thesis: Limits, regularity, and relational and weighted structures
Department: Mathematical Sciences
Advisor: James Cummings
First position: Postdoctoral Assistant Professor, Department of Mathematics, University of Michigan
 Sicun Gao
Thesis: Computable analysis, decision procedures, and hybrid automata: a new framework for the formal verification of cyberphysical systems
Department: Philosophy
Advisor: Edmund Clarke and Jeremy Avigad
First position: Postdoctoral Researcher, Computer Science Department, Carnegie Mellon University
 Rob Simmons
Thesis: Substructural Logical Specifications
Department: Computer Science
Advisor: Frank Pfenning
2010
 Peter Lumsdaine
Thesis: Higher categories from type theory
Department: Mathematical Sciences
Advisor: Steve Awodey
First position: Postdoctoral fellow, Department of Mathematics,
Dalhouse University, Halifax
 Matthew Szudzik
Thesis: Some applications of recursive functionals to the foundations of mathematics and physics
Department: Mathematical Sciences
Advisor: Richard Statman
First position: Assistant Teaching Professor, Mathematics, CMUQatar
2009
 Fritz Obermeyer
Thesis: Automated equational reasoning in nondeterministic λcalculi modulo theories H^{*}
Department: Mathematical Sciences
Advisor: Richard Statman
Later position: Google
2008
 Henrik Forsell
Thesis: FirstOrder Logical Duality
Department: Philosophy
Advisor: Steve Awodey
First position: Postdoctoral fellow, Eduard Cech Center for Mathematical
Research, Brno, Cech Republic
 Henry Towsner
Thesis: Some Results in Logic and Ergodic Theory
Department: Mathematical Sciences
Advisor: Jeremy Avigad
First position: Assistant Professor, Department of Mathematics, UCLA;
Participant in MSRI semester in Ergodic Theory and Additive
Combinatorics
Later position: Associate Professor, Department of Mathematics, University of Pennsylvania
 Michael Warren
Thesis: Homotopy Theoretic Aspects of Constructive Type
Theory
Department: Philosophy
Advisor: Steve Awodey
First position: Fields Institute Postdoc, University of
Ottawa
 Yimu Yin
Thesis: Sets, models, and valued fields
Department: Philosophy
Advisor: Jeremy Avigad
First position: Assistant Professor, Department of Mathematics,
University of Pittsburgh
2007
 Frederick Eberhardt
Thesis: Causation and Intervention
Department: Philosophy
Advisor: Richard Scheines and Clark Glymour
Later position: Professor, California Institute of Technology
 Giacomo Sillari
Thesis: Convention, Awareness and Games
Department: Philosophy
Advisor:Cristina Bicchieri and Horacio Arlo Costa
Later position: Postdoctoral Fellow, Program in Philosophy, Politics, and Economics, University of Pennsylvania
 Joshua Dunfield
Thesis: A unified system of type requirements
Department: Computer Science
Advisor: Frank Pfenning
Later position: Postdoctoral Fellow, McGill University
 Nishant Sinha
Thesis: Automated Compositional Analysis for Checking Component Substitutability
Department: Electrical and Computer Engineering
Advisor: Ed Clarke
Later position: NEC
 Pankajkumar Punjabrao Chauhan
Thesis: Verification of Large Industrial Circuits Using SAT Based Reparameterization and Automated AbstractionRefinement
Department:Computer Science
Advisor:Ed Clarke
Later position: Calypto
2006
 Anubhav Gupta
Thesis: Learning Abstractions for Model Checking
Department: Computer Science
Advisor: Ed Clarke
Later position: Cadence Research Laboratories
 Murali Talupur
Thesis: Handling Unboundedness: Abstraction Techniques for Parameterized and Real Time Verification
Department: Computer Science
Advisor: Ed Clarke
Later position: Intel
 Kaustuv Chaudhuri
Thesis: Theorem proving with the inverse method for linear logic
Department: Computer Science
Advisor: Frank Pfenning
Later position: Postdoctoral Fellow, INRIAFuturs, France
 John Mumma
Thesis: Intuition formalized: ancient and modern methods of proof in elementary geometry
Department: Philosophy
Advisor: Dana Scott
First position: Postdoctoral fellow, Ideals of Proof project, Paris
Later position: Associate Professor, Philosophy, Cal State San Bernardino
 Jiji Zhang
Thesis: Causal inference and reasoning in causally insufficient systems
Department: Philosophy
Advisor: Peter Spirtes
Later position: Assistant Professor,
Department of Philosophy, California Institute of Technology
2005
 Dirk Schlimm
Thesis: Axiomatics as engine for driving discovery in mathematics and science
Department: Philosophy
Advisor: Clark Glymour
Later position: Associate Professor,
Department of Philosophy, McGill University
 Rowan Davies
Thesis: Practical refinementtype checking
Department: Computer Science
Advisor: Frank Pfenning
Later position: Associate Lecturer, University of Western Australia
2004
 Chad Brown
Thesis: Set comprehension in Church's type theory
Department: Mathematical Sciences
Advisor: Peter Andrews
Later position: Universität des Saarlandes in Saarbrücken
 Alexei Kolesnikov
Thesis: Generalized amalgamation in simple theories and characterization of dependence relations in nonelementary classes
Department: Mathematical Sciences
Advisor: Rami Grossberg
First position: Postdoctoral Assistant Professor, University of
Michigan
Later position: Professor, Mathematics, Towson University
 Aleks Nanevski
Thesis: Functional programming with names and necessity
Department: Computer Science
Advisor: Frank Pfenning
Later position: Microsoft Research, Cambridge
 Kerry Ojakian
Thesis: Combinatorics in bounded arithmetic
Department: Mathematical Sciences
Advisor: Jeremy Avigad
First positions: Postdoc Charles University (Prague);
Postdoc, Center for Logic and Computation (Lisbon)
Later position: Associate Professor, Bronx Community College, CUNY
 Ksenija Simic (Muller)
Thesis: Aspects of ergodic theory in subsystems of secondorder arithmetic
Department: Mathematical Sciences
Advisor: Jeremy Avigad
First position: Postdoc, Mathematics, University of Arizona
Later position: Associate Professor, Mathematics, Pacific Lutheran University
2003
 Tianjiao Chu
Thesis: Learning from the SAGE data
Department: Philosophy
Advisor: Peter Spirtes
Later position: Research Scientist, Clairvoyance Corporation
 Jeffrey Helzner
Thesis: Relaxing ordering assumptions in additive conjoint measurement
Department: Philosophy
Advisor: Teddy Seidenfeld
Later position: Assistant Professor, Department of Philosophy,
Columbia University
 John Krueger
Thesis: Saturated ideals
Department: Mathematical Sciences
Advisor: James Cummings
First positions: Postdoc, University of Vienna;
Morrey Assistant Professor, University of California, Berkeley
Later position: Professor, Mathematics, North Texas State University
 Brigitte Pientka
Thesis: Tabled higherorder logic programming
Department: Computer Science
Advisor: Frank Pfenning
Later position: Professor,
Department of Computer Science, McGill University
 Mark Ravaglia
Thesis: Explicating the finitist standpoint
Department: Philosophy
Advisor: Wilfried Sieg
Later position: Faculty,
Hawaiian Preparatory Academy
2002
 Monica VanDieren
Thesis: Categoricity and stability in abstract elementary classes
Department: Mathematical Sciences
Advisor: Rami Grossberg
First positions: Szego Assistant Professor, Mathematics, Stanford University;
Hildebrandt Assistant Professor, Mathematics, University of Michigan
Later position: University Professor of Mathematics and Director,
Honors Program, Robert Morris University
2001
 Andrej Bauer
Thesis: The realizability approach to computable analysis and topology
Department: Computer Science
Advisor: Dana Scott
Later position: Professor of Computational Mathematics, University of Ljubljana, Slovenia
 Jesse Hughes
Thesis: A study of algebras and Coalgebras
Department: Philosophy
Advisors: Steve Awodey and Dana Scott
Later position: Adjunct Professor, Salem State College
 Jeff Polakow
Thesis: Ordered linear logic and applications
Department: Computer Science
Advisor: Frank Pfenning
Later position: Deutsche Bank, New York City
2000
 Barbara Kauffmann
Thesis: Application of proof theory to computational complexity: comparison of different methods
Department: Philosophy
Advisor: Wilfried Sieg
After graduating, served as adjunct professor, Carnegie Mellon University, Department of Philosophy
 Alberto Momigliano
Thesis: Elimination of negation in a logical framework
Department: Philosophy
Advisor: Frank Pfenning
Later position: Research Fellow, Computer Science, University of Edinburgh
 Gerald Penn
Thesis: The algebraic structure of attributed type signatures
Department: Language Technologies Institute
Advisors: Bob Carpenter and Frank Pfenning
Winner of the 2001 E. W. Beth Dissertation Award
Later position:
Associate Professor of Computer Science, Unversity of Toronto
 Carsten Schuermann
Thesis: Automating the metatheory of deductive systems
Department: Computer Science
Advisor: Frank Pfenning
Later position:
Associate Professor of Computer Science, IT University, Copenhagen
1999
 Lars Birkedal
Thesis: Developing theories of types and
computability via realizability
Department: Computer Science
Advisor: Dana Scott
Later position: Professor and Head of the Programming, Logic,
and Semantics Group, IT University of Copenhagen
 Matthew Bishop
Thesis: Mating search without path enumeration
Department: Mathematical Sciences
Advisor: Peter Andrews
Later position: Azlan Group Limited, England
 John Byrnes
Thesis: Proof search and normal forms in natural deduction
Department: Philosophy
Advisor: Wilfried Sieg
Later position: Principal Computer Scientist, Advanced Analytics Group of the Artificial Intelligence Center, SRI International
 Roberto Virga
Thesis: Higherorder rewriting with dependent types
Department: Mathematical Sciences
Advisor: Frank Pfenning
1998
 Olivier Lessmann
Thesis: Dependence relations in nonelementary classes
Department: Mathematical Sciences
Advisor: Rami Grossberg
First positions: Research Assistant Professor, Mathematics,
University of Illinois, Chicago; Postdoc, Mathematics, Oxford University
 Hongwei Xi
Thesis: Dependent types in practical programming
Department: Mathematical Sciences
Advisor: Frank Pfenning
Later position: Assistant Professor, Department of Computer Science, Boston University
1997
 Oliver Schulte
Thesis: Hard choices in scientific inquiry
Department: Philosophy
Advisor: Kevin Kelly
Later position: Associate Professor, School of Computing Science,
Simon Fraser University
1996
 Christopher Meek
Thesis: Selecting graphical models: causal and statistical modeling
Department: Philosophy
Advisor: Peter Spirtes
Later position: Principal Researcher in Machine Learning and Applied Statistics Microsoft Research
 Thomas Richardson
Thesis: Feedback models: interpretation and discovery
Department: Philosophy
Advisor: Peter Spirtes
Later position: Professor, Department of Statistics,
University of Washington
1995
 Michel Schellekens
Thesis: The Smyth completion: a common topological foundation for denotational semantics and complexity analysis
Department: Mathematical Sciences
Advisor: Stephen Brookes
Later position: University College Cork, Ireland, Department of Computer Science
1994
 Tim Freeman
Thesis: Refinement types for ML
Department: Computer Science
Advisor: Frank Pfenning
 Jiri Sgall
Thesis: Online scheduling on parallel machines
Department: Computer Science
Advisor: Steve Rudich
Later position: Researcher,
Academy of Sciences, Mathematical Institute, Prague
 Kim Ritter Wagner
Thesis: Solving Domain Equations with Internal PreOrders
Department: Computer Science
Advisor: Dana Scott
 Jeffrey Todd Wilson
Thesis: The assembly tower and some categorical and algebraic aspects
of frame theory
Department: Computer Science
Advisor: Dana Scott
1993
 Penny Anderson
Thesis: Program development by proof transformation
Department: Computer Science
Advisor: Frank Pfenning
 Doug Ensley
Thesis: Measures on aleph0 categorical structures
Department: Mathematical Sciences
Advisor: Michael Albert
Later position: Deputy Executive Director of the MAA
 Nevin Heintze
Thesis: Set based program analysis
Department: Computer Science
Advisors: Peter Lee and Frank Pfenning
1992
 Spiro Michaylov
Thesis: Design and implementation of practical constraint logic programming systems
Department: Computer Science
Advisor: Frank Pfenning
Later position: Ab Initio
1991
 Scott Dietzen
Thesis: A language for higherorder explanationbased learning
Department: Computer Science
Advisor: Frank Pfenning
Later position: CEO, Pure Storage
 Sunil Issar
Thesis: Operational issues in automated theorem proving using matings
Department: Mathematical Sciences
Advisor: Peter Andrews
Later position: Convergys
 Marko Petkovsek
Thesis: Finding closedform solutions of difference equations by
symbolic methods
Department: Computer Science
Advisor: Dana Scott
Later position: Faculty of Mathematics and Physics,
Department of Mathematics, Ljubljana, Slovenia
 Enrico Tronci
Thesis: Equational programming in lambdacalculus via SLsystems
Department: Mathematical Sciences
Advisor: Richard Statman
Later position: Associate Professor in Dipartimento di Informatica,
Università di Roma "La Sapienza"
1990
 Conal Elliott
Thesis: Extensions and applications of higherorder unification
Department: Computer Science
Advisor: Frank Pfenning
1988
 Vijay Anand Saraswat
Thesis: Concurrent constraint programming languages
Department: Computer Science
Advisor: Dana Scott
Later positions: Member of the Research Staff,
IBM T. J. Watson Research Lab; Adjunct Professor of Computer Science and Engineering
Penn State University
1987
 Frank Pfenning
Thesis: Proof Transformations in HigherOrder Logic
Department: Computer Science
Advisor: Peter Andrews
Later position: President's Professor of Computer Science,
Carnegie Mellon University, and Head, Department of Computer Science
1985
 Ketan Mulmuley
Thesis: Full abstraction and semantic equivalence
Department: Computer Science
Advisor: Dana Scott
Later position: Professor, Department of Computer Science, and Professor, Physical Sciences Collegiate Division,
University of Chicago
