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.
2018
 Robert Lewis
Thesis: Two tools for formalizing mathematical proofs
Department: Philosophy
Advisor: Jeremy Avigad
First position: Postdoctoral fellow, Theoretical Computer Science, Vrije Universiteit Amsterdam
 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:
Department: Mathematical Sciences
Advisor: Clinton Conley
First position:
NSF Mathematical Sciences Postdoctoral Research Fellowship,
Institut de Mathématiques,
Université Paris Diderot, France
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, Harvard University
2016
 Jacob Davis
Thesis: Universal graphs at ℵ_{ω1} and settheoretic geology Department: Mathematical Sciences
Advisor: James Cummings
First position: Google Zurich
 Sarah Loos
Thesis: Differential Refinement Logic
Department: Computer Science Department
Advisor: André Platzer
First positions: 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
 Rebecca Morris
Thesis: Appropriate steps: a theory of motivated proofs
Department: Philosophy
Advisor: Jeremy Avigad
First position: Instructor, Department of Philosophy, Carnegie Mellon University
2014
 Will Boney
Thesis: Advances in classification theory for abstract elementary classes
Department: Mathematical Sciences
Advisor: Rami Grossberg
First positions: NSF Postdoctoral Research Fellowship, University of Illinois at Chicago, followed by a Benjamin Peirce Fellowship, 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
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
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 of Mathematics, Carnegie Mellon University in Qatar
2009
 Fritz Obermeyer
Thesis: Automated equational reasoning in nondeterministic λcalculi modulo theories H^{*}
Department: Mathematical Sciences
Advisor: Richard Statman
Current 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
Current position: Assistant 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 postdoctoral position, 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
Currently James S. McDonnell Postdoc in Philosophy, University of California, Berkeley
 Giacomo Sillari
Thesis: Convention, Awareness and Games
Department: Philosophy
Advisor:Cristina Bicchieri and Horacio Arlo Costa
Currently 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
Currently a postdoctoral fellow at McGill University
 Nishant Sinha
Thesis: Automated Compositional Analysis for Checking Component Substitutability
Department: Electrical and Computer Engineering
Advisor: Ed Clarke
Currently at NEC
 Pankajkumar Punjabrao Chauhan
Thesis: Verification of Large Industrial Circuits Using SAT Based Reparameterization and Automated AbstractionRefinement
Department:Computer Science
Advisor:Ed Clarke
Currently at Calypto
2006
 Anubhav Gupta
Thesis: Learning Abstractions for Model Checking
Department: Computer Science
Advisor: Ed Clarke
Currently at Cadence Research Laboratories
 Murali Talupur
Thesis: Handling Unboundedness: Abstraction Techniques for Parameterized and Real Time Verification
Department: Computer Science
Advisor: Ed Clarke
Currently at Intel
 Kaustuv Chaudhuri
Thesis: Theorem proving with the inverse method for linear logic
Department: Computer Science
Advisor: Frank Pfenning
Currently postdoctoral fellow at 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
Current position: Postdoctoral Research fellow, Philosophy, Stanford University
 Jiji Zhang
Thesis: Causal inference and reasoning in causally insufficient systems
Department: Philosophy
Advisor: Peter Spirtes
Currently 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
Currently Associate Professor, Department of Philosophy, McGill University
 Rowan Davies
Thesis: Practical refinementtype checking
Department: Computer Science
Advisor: Frank Pfenning
Currently Associate Lecturer at the University of Western Australia
2004
 Chad Brown
Thesis: Set comprehension in Church's type theory
Department: Mathematical Sciences
Advisor: Peter Andrews
Currently at 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 at the University of
Michigan
Current position: Associate Professor at Towson University
 Aleks Nanevski
Thesis: Functional programming with names and necessity
Department: Computer Science
Advisor: Frank Pfenning
Currently at Microsoft Research, Cambridge
 Kerry Ojakian
Thesis: Combinatorics in bounded arithmetic
Department: Mathematical Sciences
Advisor: Jeremy Avigad
First positions: postdoctoral position at Charles University (Prague);
postdoctoral position at the Center for Logic and Computation (Lisbon)
Current position: Assistant Professor, Bronx Community College (C.U.N.Y.)
 Ksenija Simic (Muller)
Thesis: Aspects of ergodic theory in subsystems of secondorder arithmetic
Department: Mathematical Sciences
Advisor: Jeremy Avigad
First position: postdoc at the University of Arizona, Department of Mathematics
Current position: Assistant Professor, Mathematics, Pacific Lutheran University
2003
 Tianjiao Chu
Thesis: Learning from the SAGE data
Department: Philosophy
Advisor: Peter Spirtes
Currently a research scientist,
Clairvoyance Corporation
 Jeffrey Helzner
Thesis: Relaxing ordering assumptions in additive conjoint measurement
Department: Philosophy
Advisor: Teddy Seidenfeld
Currently an Assistant Professor, Department of Philosophy, Columbia University
 John Krueger
Thesis: Saturated ideals
Department: Mathematical Sciences
Advisor: James Cummings
After graduating, was a postdoc at the University of Vienna and a Morrey Assistant Professor at University of California, Berkeley.
Currently an Assistant Professor at North Texas State University.
 Brigitte Pientka
Thesis: Tabled higherorder logic programming
Department: Computer Science
Advisor: Frank Pfenning
Currently Associate Professor, Department of Computer Science, McGill University
 Mark Ravaglia
Thesis: Explicating the finitist standpoint
Department: Philosophy
Advisor: Wilfried Sieg
Currently on the faculty of the
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, Stanford University
and Hildebrandt Assistant Professor, University of Michigan
Current position: University Professor of Mathematics and Director,
Honors Program at Robert Morris University
2001
 Andrej Bauer
Thesis: The realizability approach to computable analysis and topology
Department: Computer Science
Advisor: Dana Scott
Currently Assistant Professor of Mathematics and Computer Science at the University of Ljubljana, Slovenia
 Jesse Hughes
Thesis: A study of algebras and Coalgebras
Department: Philosophy
Advisors: Steve Awodey and Dana Scott
Currently adjunct professor of philosophy at Salem State College in Salem, MA
and Bentley College in Waltham, MA
 Jeff Polakow
Thesis: Ordered linear logic and applications
Department: Computer Science
Advisor: Frank Pfenning
Currently at 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
Currently a research fellow in 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.
Currently Associate Professor of Computer Science at the Unversity of Toronto.
 Carsten Schuermann
Thesis: Automating the metatheory of deductive systems
Department: Computer Science
Advisor: Frank Pfenning
Currently 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
Currently Professor and head of the Programming, Logic, and Semantics group at the IT University of Copenhagen
 Matthew Bishop
Thesis: Mating search without path enumeration
Department: Mathematical Sciences
Advisor: Peter Andrews
Currently at Azlan Group Limited, England
 John Byrnes
Thesis: Proof search and normal forms in natural deduction
Department: Philosophy
Advisor: Wilfried Sieg
Principal Computer Scientist, Advanced Analytics Group of the Artificial Intelligence Center at 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
After graduating, was a Research Assistant Professor, Department of Mathematics,
University of Illinois, Chicago, and then a postdoc at Oxford University
 Hongwei Xi
Thesis: Dependent types in practical programming
Department: Mathematical Sciences
Advisor: Frank Pfenning
Currently Assistant Professor, Department of Computer Science, Boston University
1997
 Oliver Schulte
Thesis: Hard choices in scientific inquiry
Department: Philosophy
Advisor: Kevin Kelly
Currently 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
Currently a principal researcher in Machine Learning and Applied Statistics at Microsoft Research
 Thomas Richardson
Thesis: Feedback models: interpretation and discovery
Department: Philosophy
Advisor: Peter Spirtes
Currently 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
Currently at 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
Currently 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
Currently Professor of Mathematics at Shippensburg University, Department of Mathematics
 Nevin Heintze
Thesis: Set based program analysis
Department: Computer Science
Advisors: Frank Pfenning and Peter Lee
1992
 Spiro Michaylov
Thesis: Design and implementation of practical constraint logic programming systems
Department: Computer Science
Advisor: Frank Pfenning
Currently at Ab Initio
1991
 Scott Dietzen
Thesis: A language for higherorder explanationbased learning
Department: Computer Science
Advisor: Frank Pfenning
Currently CEO at Pure Storage
 Sunil Issar
Thesis: Operational issues in automated theorem proving using matings
Department: Mathematical Sciences
Advisor: Peter Andrews
Currently at Convergys
 Marko Petkovsek
Thesis: Finding closedform solutions of difference equations by
symbolic methods
Department: Computer Science
Advisor: Dana Scott
Currently on the 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
Currently 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
Currently member of the Research Staff,
IBM T. J. Watson Research Lab, and 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
Currently President's Professor of Computer Science at Carnegie Mellon University, and Head, Department of Computer Science
1985
 Ketan Mulmuley
Thesis: Full abstraction and semantic equivalence
Department: Computer Science
Advisor: Dana Scott
Currently Professor, Department of Computer Science, and Professor, Physical Sciences Collegiate Division,
University of Chicago.
