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
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
system for more details.
Click on titles for abstracts
and postscript versions
Modal Analysis of Staged Computation, Journal of the ACM,
48(3):555-604, 2001. (Joint work with Frank Pfenning).
Types and Computational Effects, International Conference on Functional
Programming (ICFP'2000), Montreal, Canada, September 2000. (Joint
work with Frank Pfenning.)
Judgmental Reconstruction of Modal Logic, Mathematical Structures
in Computer Science, 11(4), August 2001. (Joint work
with Frank Pfenning.)
Types as Staging Specifications for Run-time Code Generation, ACM
Computing Surveys, 30(3es), 1998. (Joint work with Philip
Wickline, Peter Lee, Frank
Refinement-Type Checking. Thesis proposal, Carnegie-Mellon University,
Refinement-Type Checker for Standard ML, Sixth International
Conference on Algebraic Methodology and Software Technology (AMAST'97),
Sydney, Australia, December 1997.
Combinators for Web Computing, IEEE Transactions on Software
Engineering, 25(3), May/June 1999. A conference version appeared
at USENIX Conference on Domain-Specific
Languages (DSL'97), Santa Barbara, California, October, 1997. Another
version appears as Research
Report 148, Digital Equipment Corporation Systems Research Center,
Palo Alto, CA, June 1997. (Joint work with Luca
Temporal Logic Approach to Binding-Time Analysis, In E. Clarke,
editor, Proceedings of the Eleventh Annual Symposium on Logic in Computer
Science (LICS'96), pages 184-195, July 1996.
Modal Analysis of Staged Computation, 23rd Annual ACM Symposium
on Principles of Programming Languages (POPL'96), pages 258-270, January
1996. An earlier version appeared in the workshop on Types
for Program Analysis, Aarhus, Denmark, May 1995. A greatly
extended version is also available (see above). (joint work with Frank
domination, tabu search and the football pool problem, Discrete
Applied Mathematics 74(3):217-228, 1997. (joint work with Gordon
- A photo of me.
tree which was put together by my brother Mark.
Braille Knitting & Crochet Patterns & Recipes, a web page which
I helped put together.
Project at INRIA
- Rocquencourt, France where I had a great time working in the summer
BRICS, at DAIMI
in the University of Aarhus, Denmark, where I had another great time in
the summer of '95.
Research Center, where I was a summer intern for the summer of '96,
and had yet another wonderful time.
Programming Languages page. Very useful for PL researchers.
my home country, as seen by the CIA (lots of general information like population,
Australia as seen
by people on the net (a hypertext FAQ).
home city, as seen from across the Swan River.