Former PhD Students
First Steps in Synthetic Tait Computability.
Ph.D., October 2021.
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. Recipient of the 2017 Carnegie Mellon University School of Computer
Science Dissertation Award.
- Dan Licata. Dependently Typed Programming with
Domain-Specific Logics, February 2011. Co-winner 2012 Beth
Modeling Frameworks for the Optimization of Discrete-Continuous
Systems. (Co-advisor: Ignacio Grossmann, Chemical
- Umut Acar.
Computation. May, 2005. (Co-advisor: Guy Blelloch.)
Cheng. Scalable Real-Time
Parallel Garbage Collection for Symmetric
Multiprocessors. September, 2001. (Co-advisor: Guy
- Derek Dreyer.
Understanding and Evolving
the ML Module System/ May, 2005. (Co-advisor: Karl
Effects. May, 1996. (Co-advisor: John
Lillibridge . Translucent Sums: A Foundation
for Higher-Order Module Systems . May, 1997.
With Types . December, 1995. (Co-advisor: Jeannette
- 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.)
Pierce. Programming with
Intersection Types and Bounded Polymorphism .
December, 1991. (Co-advisor: John Reynolds.)
- Daniel Spoonhower. Scheduling Deterministic Parallel
Programs. (Co-advisor: Guy Blelloch.)
Stone. Singleton Kinds and
Singleton Types . August, 2000.
Member of PhD Thesis Committee
- 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.
Davies. Practical Refinement-Type
Checking. May, 2005.
Dunfield. A Unified System of Type Refinements.
- 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,
- 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.
Programming with Names and Necessity. August,
Necula. Compiling with
Proofs . September, 1998.
Functional Data Structures . September, 1996.
- Sungwoo Park.
A Programming Language for
Probabilistic Computation . August, 2005.
Higher-Order Logic Programming . December,
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,
- Robert J. Simmons.
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
Last modified: Tue Sep 28 22:01:35 EDT 2021