I'm interested in program analysis and
transformation, with a particular emphasis on program
verification, correctness by construction, dependent and
otherwise fancy type systems, and functional languages.
My advisor is the inimitable, indefatigable, inestimable, indescribable Ranjit Jhala.
Publications
Type-Based Data Structure Verification (PLDI 2009)
We present a refinement type-based approach for the static verification of complex data structure invariants which permits liquid type inference to automatically synthesize complex invariants from simple logical qualifiers, thereby almost completely automating the verification.
Liquid Types (PLDI 2008)
We present Logically Qualified Data Types, abbreviated to Liquid Types, a system that combines Hindley-Milner type inference with Predicate Abstraction to automatically infer dependent types precise enough to prove a variety of safety properties.
Projects
Dsolve
Dsolve is our type inference tool which extends OCaml's type system with liquid types and type-based data structure verification.
Software
¡Voila!
¡Voila! is a Python script for creating animated presentations in Inkscape. It allows you to create animated slides using Inkscape layers and a simple description file, then outputs a series of SVG images which can be viewed with Inkview.
Mondrian Clock
Mondrian Clock is a program for generating random Mondrian-style pictures. These pictures happen to depend on the time of day in a convoluted way; with some practice, it can be used as a fuzzy clock.
ChitChat
ChitChat is a sandbox for toying with Javascript and the canvas element.
Oyices
Oyices is an OCaml binding for the yices theorem prover. The binding is an overlay over the yices Linux binary distribution. Bill Harris contributed support for bitvector functions.