Rowan Davies

Associate Lecturer in the School of Computer Science & Software Engineering at the University of Western Australia.


In the second semester of 2007 I expect to be involved in the teaching of:
  • CITS3211 Functional Programming
  • CITS3241 Robotics
  • Research

    My research focuses on programming and languages, using concepts from logic and type theory.  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.  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 features of ordinary type systems such as functions and records with elements of program properties such as 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 extending the programming language Standard ML with refinement-type checking.  Here are some examples of programming with refinement types.  See my thesis proposal for more details.

    Recent Papers                     Click on titles for abstracts and postscript versions

    A Modal Analysis of Staged Computation, Journal of the ACM, 48(3):555-604, 2001.  (Joint work with Frank Pfenning).

    Intersection Types and Computational Effects, International Conference on Functional Programming (ICFP'2000), Montreal, Canada, September 2000.  (Joint work with Frank Pfenning.)

    A Judgmental Reconstruction of Modal Logic, Mathematical Structures in Computer Science, 11(4), August 2001.  (Joint work with Frank Pfenning.)

    Modal Types as Staging Specifications for Run-time Code Generation, ACM Computing Surveys, 30(3es), 1998. (Joint work with Philip Wickline, Peter Lee, Frank Pfenning.)

    Practical Refinement-Type Checking. Thesis proposal, Carnegie-Mellon University, December 1997.

    A Practical Refinement-Type Checker for Standard ML, Algebraic Methodology and Software Technology (AMAST'97), Sydney, Australia, December 1997.

    Service Combinators for Web Computing, IEEE Transactions on Software Engineering, 25(3), May/June 1999.  (Joint work with Luca Cardelli.)

    A Temporal Logic Approach to Binding-Time Analysis, Logic in Computer Science (LICS'96), pages 184-195, July 1996.

    A Modal Analysis of Staged Computation, Principles of Programming Languages (POPL'96), pages 258-270, January 1996.  A greatly extended version is also available (see above).  (joint work with Frank Pfenning).

    Graph domination, tabu search and the football pool problem, Discrete Applied Mathematics, 74(3):217-228, 1997. (joint work with Gordon Royle).

    Various links

    Rowan Davies