Rowan Davies: Research Interests

Summary:

My research interests mostly concern the examination of the wide variety of concepts in both theoretical and practical computer science and attempting to relate these to concepts in logic and type theory.  This sometimes leads to new insights, and sometimes suggests useful generalizations of computer science concepts.  For example, in ongoing work with others I have demonstrated a relationship between modal logics and the languages used in partial evaluation, and used this idea to design an extension of the programming language ML with run-time code generation.  Recently my main interest has been refinement types, which allow efficient expression of many common program properties that are beyond the scope of ordinary type systems, while retaining desirable properties such as an intuitive error reporting, and efficient checking.
 

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.