Current PhD Students

• Avijit Kumar. Languages for Authenticated Mobile Computing.
• Daniel K. Lee. Mechanizing Language Definitions.
• Dan Licata. Dependent refinement types.

Former PhD Students

• 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

• 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. Refinement Types for ML. Expected: May, 2005.
• Joshua Dunfield. Unifying Principles of Type Refinements. Expected: December, 2005.
• Deepak Garg. Logic-Based Authorization. March, 2008.
• 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 LF. March, 2008.
• 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 . Expected: May, 2005.
• Brigitte Pientka. Tabled Higher-Order Logic Programming . December, 2003.
• Jeff Polakow. Ordered Linear Logic and Applications . August, 2001.
• Jason Reed. A Hybrid Metalogical Framework. February, 2007.
• Susmit Sarkar. A Dependently Typed Programming Language, with Applications to Foundational Certified Code Systems. May, 2009.
• 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.

Current Undergraduate Students

• Arbob Ahmad.Focusing on Equivalence for Sum Types.

Former Undergraduate Students

• 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: Fri Jun 3 14:22:00 EDT 2005