Rowan Davies

After many years, I have now finally completed my Ph.D. in the CS department at CMU (advised by Frank Pfenning).  I'm now a lecturer and researcher in the School of Computer Science & Software Engineering at the University of Western Australia. The following is thus out of date, and you should see my home page at UWA if you want to find out what I've been up to more recently.

Research

My research focuses on applications of logic and type theory to programming and languages.  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 a form of typed "staged computation", including a form of run-time code generation.  In separate work I have considered modal logic as a logical basis for languages which combine imperative features and more "logical" constructs such as functions and pairs.  See my longer description of research interests for more details.

Recently my main interest has been refinement types, which combine the features of ordinary type systems such as function and record types with elements of program properties such as implication and logical "and".  This allows 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.  My thesis work involves building a refinement type checker for the Standard ML programming language.  See my thesis summary and the home page for the SML CIDRE system for more details.

Recent Papers       Click on titles for abstracts and postscript versions

Various links

Rowan Davies
rowan@cs.cmu.edu