In Depth:

Broadly my research interests are centered on the relationship between computer science and logic.  More specifically, I am interested in the application of mathematical logic and type theory to the design, analysis and implementation of programming languages.  Some general interests include the following list, which very roughly starts with fundamentals and ends with applications: natural deduction, intuitionistic logic, modal and temporal logics, applications of the  Curry-Howard isomorphism, typed calculi and languages, monadic approaches to effects, modal and temporal types, intersection types, subtyping, refinement types, logical frameworks, logic programming, functional programming, imperative programming, object-oriented programming, software and hardware verification, staged languages, run-time code generation, partial evaluation, and web programming.

Recently my main interest has been refinement types, which combine the features of ordinary type systems such as functions and records with elements of program properties such as implication and logical "and".  My thesis work concentrates on extending Standard ML with a form of refinement types that includes intersection types, which correspond to logical conjunction of properties, and subsets of ML datatypes defined by regular tree grammars.   My refinement checker takes advantage of simple refinement annotations in natural places such as module boundaries to allow efficient checking.  The checker is essentially a type checker that avoids duplicating work by generating and checking quantified boolean formulae, a technique similar to that used very successfully in hardware verification.  The experience so far is quite positive: these refinements seem to be expressive enough to be useful, simple enough to comprehend when reading and writing programs, and the checker is efficient enough to run every time a program is compiled.  One of my main areas of interest is in exploring what other program properties can be naturally captured and efficiently checked by adding more features to refinement types, e.g. modalities for imperative properties, and dependent types for array bounds (and much more).

Another interest of mine is applications of typed languages with modal and temporal types, i.e. the image of modal and temporal logics under the Curry-Howard isomorphism.  One view of these languages is that they allow programs which manipulate program fragments as data.  Instances of this are macros, partial evaluation, and run-time code generation, which broadly fit under the heading "staged computation".  A particular interest of mine is the extension of the language ML with run-time code generation.

A different view of languages with modal types is that they form a logical basis for languages which combine imperative features and more "logical" constructs such as functions and pairs.  This builds on work by others which relates lax logic to the monadic metalanguage, a language based on category theory which also combines imperative features and functions.  A particular interest of mine is to combine this idea with refinement types to try to design a practical system for expressing and checking common imperative properties of programs.