Alumni
The following is a partial list of students who earned a PhD in Computer Science, Mathematical Sciences, or Philosophy, and wrote a dissertation in a logic-related area under the supervision of a member of the PAL faculty.
2024- Wei Dai
Thesis: Ergodic Aspects of Graphing Equivalence Relations
Department: Mathematical Sciences
Advisor: Clinton Conley
First position: Postdoc, Nankai University, China
- David Kahn
Thesis: Leveraging Linearity to Improve Automatic Amortized Resource Analysis
Department: Computer Science
Advisor: Jan Hoffmann
First position: Assistant Professor, Denison University
- Pedro Marun
Thesis: Spaces, Trees and Labelled Sets
Department: Mathematical Sciences
Advisor: James Cummings
First position: Postdoc, Czech Academy of Sciences, Prague
- Klaas Pruiksma
Thesis: Adjoint Logic with Applications
Department: Computer Science
Advisor: Frank Pfenning
First position: Postdoc, Institue of Information Security, University of Stuttgart
- Siva Somayyajula
Thesis: Total Correctness Type Refinements for Communicating Processes
Department: Computer Science
Advisor: Frank Pfenning
First position: Researcher at Amazon Web Services
- Felix Weilacher
Thesis: Definable Combinatorics in Descriptive Set Theory, Computability Theory, and Beyond
Department: Mathematical Sciences
Advisor: Clinton Conley
First position: National Science Foundation (NSF) Mathematical Sciences Research Fellow, University of California, Berkeley
- Wentao Yang
Thesis: On Successive Categoricity, Stability and NIP in Abstract Elementary Classes
Department: Mathematical Sciences
Advisor: Rami Grossberg
First position: Researcher, Inner Mongolia University, China
- Katherine Kosaian
Thesis: Formally Verifying Algorithms for Real Quantifier Elimination
Department: Computer Science
Advisor: André Platzer
First position: Postdoc, Iowa State University
Starting Fall, 2024: Assistant Professor, Computer Science, University of Iowa
- Samson Leung
Thesis: Stability, Categoricity and Axiomatization of Abstract Elementary Classes
Department: Mathematical Sciences
Advisor: Rami Grossberg
2022 Mathematical Sciences Outstanding Research Graduate Student Prize
2023 MCS Hugh D. Young Graduate Student Teaching Award
First position: Assistant Teaching Professor, Department of Mathematics, Penn State University
- Colin Zwanziger
Thesis: The natural display topos of coalgebras
Department: Philosophy
Advisor: Steve Awodey
First position: Postdoc, Department of Philosophy, Charles University, Prague
Second position: Postdoc, Czech Academy of Sciences, Prague
- 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
- Shaun Allison
Thesis: Actions of Polish groups and anti-classification results
Department: Mathematical Sciences
Advisor: Clinton Conley
First position: Postdoctoral Fellow, Mathematics, Hebrew University
Second position: Postdoctoral Fellow, Mathematics, University of Toronto
- Brandon Bohrer
Thesis: Practical End-to-End Verification of Cyber-Physical Systems
Department: Computer Science
Advisor: André Platzer
First position: Assistant Professor, Worcester Polytechnic Institute
- Farzaneh Derakhshan
Thesis: Session-Typed 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
Beginning Fall, 2024: Assistant Professor, Mathematics, Chulalongkorn University
- Marcos Mazari-Armida
Thesis: Remarks on classification theory for abstract elementary classes with applications to abelian group theory and ring theory
Department: Mathematical Sciences
Advisor: Rami Grossberg
2021 Association for Symbolic Logic (ASL) Sacks Prize
First position: Burnett Meyer Postoctoral Fellow, Mathematics, University of Colorado, Boulder
Second position: Assistant Professor of Mathematics, Baylor University
- Patrick Walsh
Thesis: Categorical characterization of accessible domains
Department: Philosophy
Advisor: Wilfried Sieg
First position: Assistant Teaching Professor, CMU-Qatar
- 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, Bar-Ilan University
Beginning Fall, 2024: Assistant professor, Mathematics, North Texas State University
- Nathan Fulton
Thesis: Verifiably Safe Autonomy for Cyber-Physical Systems
Department: Computer Science
Advisor: André Platzer
First position: Researcher, MIT-IBM 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
2016 MCS Hugh D. Young Graduate Student Teaching Award
First position: Postdoctoral Lecturer, Mathematics Department, Northwestern University
Later position: Assistant Teaching Professor, Department of Mathematical Sciences, CMU
- Egbert Rijke
Thesis: Classifying types
Department: Philosophy (Pure and Applied Logic)
Advisor: Steve Awodey
First position: Postdoctoral Researcher, Mathematics Department, University of Illinois Urbana-Champaign
- 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: National Science Foundation (NSF) Mathematical Sciences Postdoctoral Research Fellowship, Institut de Mathématiques, Université Paris Diderot, France
Later position: Assistant Professor, Mathematics, University of Waterloo
- 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
2014 MCS Hugh D. Young Graduate Student Teaching Award
2017 Association for Symbolic Logic (ASL) Sacks Prize
First position: Benjamin Peirce Fellow, Mathematics, Harvard University
- Jacob Davis
Thesis: Universal graphs at ℵω1 and set-theoretic geology
Department: Mathematical Sciences
Advisor: James Cummings
First position: Google Zurich
- Kristina Sojakova
Thesis: Higher Inductive Types as Homotopy-Initial Algebras
Department: Computer Science
Advisor: Steve Awodey (Philosophy) and Frank Pfenning
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
- 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 Session-based Concurrent Computation
Department: Computer Science
Advisor: Luis Caires (Universidade Nova de Lisboa) and Frank Pfenning
- Will Boney
Thesis: Advances in classification theory for abstract elementary classes
Department: Mathematical Sciences
Advisor: Rami Grossberg
First position: Benjamin Peirce Fellowship, Mathematics, Harvard University and National Science Foundation (NSF) Postdoctoral Research Fellowship
Second position: Assistant Professor, Mathematics, Texas State University
- Spencer Breiner
Thesis: Scheme representation for first-order logic
Department: Philosophy
Advisor: Steve Awodey
First position: Postdoctoral Researcher, National Institute of Standards & Technology
- Chris Lambie-Hanson
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
Later position: Researcher, Institute of Mathematics, Czech Academy of Sciences
- 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
- 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 cyber-physical 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
- Peter Lumsdaine
Thesis: Higher categories from type theory
Department: Mathematical Sciences
Advisor: Steve Awodey
First position: Postdoctoral fellow, Department of Mathematics, Dalhouse University, Halifax
Later position: Assistant Professor, Mathematics, Stockholm University
- Matthew Szudzik
Thesis: Some applications of recursive functionals to the foundations of mathematics and physics
Department: Mathematical Sciences
Advisor: Richard Statman
2007 MCS Hugh D. Young Graduate Student Teaching Award
First position: Assistant Teaching Professor, Mathematics, CMU-Qatar
- Fritz Obermeyer
Thesis: Automated equational reasoning in nondeterministic λ-calculi modulo theories H*
Department: Mathematical Sciences
Advisor: Richard Statman
Later position: Google
- Henrik Forsell
Thesis: First-Order 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
- 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 Abstraction-Refinement
Department:Computer Science
Advisor: Ed Clarke
Later position: Calypto
- 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: Post-doctoral Fellow, INRIA-Futurs, 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
- 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 refinement-type checking
Department: Computer Science
Advisor: Frank Pfenning
Later position: Associate Lecturer, University of Western Australia
- 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 non-elementary classes
Department: Mathematical Sciences
Advisor: Rami Grossberg
2001 CMU Eberly Center Graduate Student Teaching Award
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 second-order arithmetic
Department: Mathematical Sciences
Advisor: Jeremy Avigad
2007 MCS Hugh D. Young Graduate Student Teaching Award
First position: Postdoc, Mathematics, University of Arizona
Later position: Associate Professor, Mathematics, Pacific Lutheran University
- 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 higher-order 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
- 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
- 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
- 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 meta-theory of deductive systems
Department: Computer Science
Advisor: Frank Pfenning
Later position: Associate Professor of Computer Science, IT University, Copenhagen
- 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: Higher-order rewriting with dependent types
Department: Mathematical Sciences
Advisor: Frank Pfenning
- Olivier Lessmann
Thesis: Dependence relations in nonelementary classes
Department: Mathematical Sciences
Advisor: Rami Grossberg
1996 MCS Hugh D. Young Graduate Student Teaching Award
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: Associate Professor, Department of Computer Science, Boston University
- Oliver Schulte
Thesis: Hard choices in scientific inquiry
Department: Philosophy
Advisor: Kevin Kelly
Later position: Associate Professor, School of Computing Science, Simon Fraser University
- 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
- 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
- Tim Freeman
Thesis: Refinement types for ML
Department: Computer Science
Advisor: Frank Pfenning
- Jiri Sgall
Thesis: On-line 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 Pre-Orders
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
- Penny Anderson
Thesis: Program development by proof transformation
Department: Computer Science
Advisor: Frank Pfenning
- Doug Ensley
Thesis: Measures on aleph-0 categorical structures
Department: Mathematical Sciences
Advisor: Michael Albert
1992 CMU Eberly Center Graduate Student Teaching Award
Later position: Deputy Executive Director of the MAA
Later position: Shippenburg University, Mathematics, Emeritus Professor
- Nevin Heintze
Thesis: Set based program analysis
Department: Computer Science
Advisors: Peter Lee and Frank Pfenning
- Spiro Michaylov
Thesis: Design and implementation of practical constraint logic programming systems
Department: Computer Science
Advisor: Frank Pfenning
Later position: Ab Initio
- Scott Dietzen
Thesis: A language for higher-order explanation-based 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 closed-form 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 lambda-calculus via SL-systems
Department: Mathematical Sciences
Advisor: Richard Statman
Later position: Associate Professor in Dipartimento di Informatica, Università di Roma "La Sapienza"
- Conal Elliott
Thesis: Extensions and applications of higher-order unification
Department: Computer Science
Advisor: Frank Pfenning
- 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
- Frank Pfenning
Thesis: Proof Transformations in Higher-Order Logic
Department: Computer Science
Advisor: Peter Andrews
Later position: President's Professor of Computer Science, Carnegie Mellon University, and Head, Department of Computer Science
- 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