Pure and Applied Logic

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 logic-related 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 anti-classification results
Department: Mathematical Sciences
Advisor: Clinton Conley
First position: Postdoctoral Fellow, Mathematics, Hebrew University
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
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
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, 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

2018

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
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 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: 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 ℵ_ω₁ 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
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 Session-based 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 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

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 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

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, CMU-Qatar

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: 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

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 Abstraction-Refinement
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: 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

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 refinement-type 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 non-elementary 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 second-order 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 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

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 meta-theory 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: Higher-order 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: 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

1993

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
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 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"

1990

Conal Elliott
Thesis: Extensions and applications of higher-order 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 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

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