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.

2016
  • Jacob Davis
    Thesis: Universal graphs at ℵω1 and set-theoretic 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 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
     
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
     
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: 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
    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 Abstraction-Refinement
    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 post-doctoral fellow at 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
    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 refinement-type 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 non-elementary 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 second-order 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 higher-order 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 Co-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 meta-theory 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: 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
    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: On-line 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 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
    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 higher-order explanation-based 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 closed-form 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 lambda-calculus via SL-systems
    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 higher-order 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 Higher-Order 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.