Advisor: Cormac Flanagan
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. Programming Languages meets Program Verification, 2009. 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 slides)
Proving correctness of a dynamic atomicity analysis in Coq. C Sadowski, J Yi, K Knowles, C Flanagan. Workshop on Mechanizing Metatheory 2008. (PDF Coq)
First-Order Logic à la Carte. K Knowles. The Monad Reader Issue 11 2008. A demonstration of how to use explicit functor coproducts to express the structure and correctness of some transformations of first-order logic formulas.
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