Advisor: Cormac Flanagan
Associates: Stephen Freund, Aaron Tomb, Jessica Gronski, Jaeheon Yi, Caitlin Sadowski
See also my curriculum vitae and resume.
Explicit names without alpha-equivalence: Simple type soundness for a CEK semantics. K Knowles, C Flanagan. Draft 2007.
The shortest Coq proof of type soundness for the simply-typed lambda calculus, using explicit names and no custom tactics. (PDF Coq)
Compositional and Decidable Checking for Dependent Contract Types. K Knowles, C Flanagan. Tech Report UCSC-SOE-08-17 2008. A new approach to dependent types that uses existential quantification to avoid inserting arbitrary terms into types, restoring predictability to proof obligations that arise during typechecking. (PDF)
Type Reconstruction for General Refinement Types. K Knowles, C Flanagan. European Symposium on Programming, 2007.
Even though type checking for general refinement types is undecidable, type reconstruction (sometimes known as type inference) is decidable. (PDF extended slides)
Sage: Unified Hybrid Checking for First-Class Types, General Refinement Types, and Dynamic. K Knowles, A Tomb, J Gronski, C Flanagan, S Freund. Workshop on Scheme and Functional Programming, 2006.
Extended and revised; a report on a prototype of a language with Hybrid Type Checking - and a bunch of other stuff which HTC makes easier. (PDF)
See also http://sage.soe.ucsc.edu
"Functional Programming: This is how God would program. But since he doesnt exist, there's no reason to be shy." - Neil Ghani