Students

Former PhD Students

Yue Niu. Cost-sensitive Programming, Verification, and Semantics. Ph.D., September, 2024.
Jonathan Sterling. First Steps in Synthetic Tait Computability. Ph.D., October 2021. Finalist, 2022 E. W. Beth Dissertation Prize. Honorable mention, 2022 Carnegie Mellon University SCS Dissertation Award. Recipient, 2023 Edmund and Martha Clarke Computer Science Department Dissertation Award.
Evan Cavallo. Higher Inductive Types and Parametricity in Cubical Type Theory. Ph.D. February, 2021. (M.Sc. Thesis: Synthetic Cohomology in Homotopy Type Theory. December, 2015.)
Carlo Angiuli. Computational Higher-Dimensional Type Theory, September, 2019. Recipient of the 2019 Carnegie Mellon University School of Computer Science Dissertation Award. Runner-up for the 2020 E. W. Beth Dissertation Prize.
Joseph Tassarotti. Verifying Concurrent Randomized Algorithms, January, 2019. (Co-advisor: Derek Dreyer, MPI-SWS.)
Kuen-Bang Hou (Favonia). Higher-Dimensional Types in the Mechanization of Homotopy Theory, February, 2017.
Dan Licata. Dependently Typed Programming with Domain-Specific Logics, February 2011. Co-winner 2012 Beth Prize.
Ashish Agarwal. Logical Modeling Frameworks for the Optimization of Discrete-Continuous Systems. (Co-advisor: Ignacio Grossmann, Chemical Engineering)
Umut Acar. Self-Adjusting Computation. May, 2005. (Co-advisor: Guy Blelloch.)
Perry Cheng. Scalable Real-Time Parallel Garbage Collection for Symmetric Multiprocessors. September, 2001. (Co-advisor: Guy Blelloch.)
Derek Dreyer. Understanding and Evolving the ML Module System/ May, 2005. (Co-advisor: Karl Crary.)
Andrzej Filinski. Controlling Effects. May, 1996. (Co-advisor: John Reynolds.)
Mark Lillibridge . Translucent Sums: A Foundation for Higher-Order Module Systems . May, 1997.
Greg Morrisett. Compiling With Types . December, 1995. (Co-advisor: Jeannette Wing.)
Tom Murphy. Modal Types for Mobile Code. (Co-advisor: Karl Crary.)
Leaf Petersen. Certifying Compilation for Standard ML in a Type Analysis Framework. May, 2005. (Co-advisor: Karl Crary.)
Benjamin Pierce. Programming with Intersection Types and Bounded Polymorphism . December, 1991. (Co-advisor: John Reynolds.)
Daniel Spoonhower. Scheduling Deterministic Parallel Programs. (Co-advisor: Guy Blelloch.)
Christopher Stone. Singleton Kinds and Singleton Types. August, 2000.

Member of PhD Thesis Committee

Jaitin Arora. Provably Efficient Coscheduling of Computation and Memory through Disentanglement. August, 2024.
Henry DeYoung. Session-Typed Ordered Logical Specifications December, 2020.
Stefan Muller. Responsive Parallel Computation. September, 2018.
Cyrus Omar. Reasonably Programmable Syntax. May, 2017.

Eli Brandt. Temporal Type Constructors for Computer Music Programming . August, 2002.
Chris Colby. Semantics-Based Program Analysis via Symbolic Composition of Transfer Relations . August, 1996.
Rowan Davies. Practical Refinement-Type Checking. May, 2005.
Jana Dunfield. A Unified System of Type Refinements. August, 2007.
Deepak Garg. Proof Theory for Authorization Logic and its Application to a Practical File System. December, 2009.
John Greiner. Semantics-Based Parallel Cost Models and Their Use in Provably Efficient Implementations . April, 1997.
Neel Krishnaswami. Verifying Higher-Order Imperative Programs with Higher-Order Separation Logic. February, 2009.
William Lovas. Refinement Types for Logical Frameworks. August, 2010.
Sean McLaughlin. Practical Automated Theorem Proving with the Polarized Inverse Method. May, 2009.
Aleksandar Nanevski. Functional Programming with Names and Necessity. August, 2004.
George Necula. Compiling with Proofs . September, 1998.
Chris Okasaki. Purely Functional Data Structures . September, 1996.
Sungwoo Park. A Programming Language for Probabilistic Computation . August, 2005.
Brigitte Pientka. Tabled Higher-Order Logic Programming . December, 2003.
Jeff Polakow. Ordered Linear Logic and Applications. August, 2001.
Jason Reed. A Hybrid Logical Framework. August, 2009.
Susmit Sarkar. A Dependently Typed Programming Language, with Applications to Foundational Certified Code Systems. May, 2009.
Robert J. Simmons. Substructural Logic Specifications.November, 2012.
Carsten Schuermann. Automating the Meta-Theory of Deductive Systems . November, 2000.
Kevin Watkins. CLF: A Logical Framework for Concurrent Systems. Expected: 2005.
Hongwei Xi. Dependent Types in Practical Programming.. December, 1998.
Noam Zeilberger. The Logical Basis of Evaluation Order and Pattern Matching. May, 2009.

Former Undergraduate Students

Danny Gratzer. Undergraduate research on PL semantics. (Jointly advised with Karl Crary.)
Ananya Kumar. Undergraduate research on parallel functional arrays and streaming algorithms. (Jointly advised with Guy Blelloch and Avrim Blum.)
Sridhar Ramesh. ConCert Grid Infrastructure; Extending Tutch for Dual Intuitionistic Linear Logic.
Matt Kehrt. ConCert Grid Infrastructure.
Matt Moore. ConCert Grid Infrastructure.
Ruy Ley-Wild ConCert Grid Infrastructure.
David Fontaine ConCert Grid Infrastructure.
Akiva Leffert. Genetic Programming on the ConCert Grid.
Vikram Manjunath. Sabotage tolerance in ConCert.
Mickey Gupta. Implementation of a flexible, general grid computing infrastructure.
Adam Chlipala. Non-local type inference for the TILT intermediate language.
Evan Chang. Iktara in ConCert: Realizing a Certified Grid Computing Framework from a Programmer's Perspective.
Margaret Delap. Implementing a Framework for Certified Grid Computing.
Jason Liszka. LightHarp Ray Tracer for ConCert.
Karl Crary. Typing of a Practical Programming Lanugage with Higher-Kinds and Higher-Order Modules. May, 1993. Recipient of the Alan Newell Award for Undergraduate Research.

Last modified: Tue Sep 28 22:01:35 EDT 2021