| School of Computer Science &
Software Eng. University of Western Australia 35 Stirling Highway Crawley, Western Australia, 6009. |
Email: WWW: |
rowan@csse.uwa.edu.au http://www.csse.uwa.edu.au/~rowan |
| Research
Interests
Applications of mathematical logic and type theory in computer
science, particularly in the design and implementation of programming
languages. Refinement types and software verification.
Typed languages based on modal and temporal logics and their
applications to partial evaluation, runtime code generation and
imperative programming. Functional programming, imperative
programming, object-oriented programming, and web programming.
Logical frameworks and logic programming. Education |
||||
| 1993-2001 |
|
Pittsburgh, PA, USA
|
||
| (2001-2005 in absentia) | ||||
| M.S. in Computer Science (Pure
and Applied Logic), December 1995. Ph.D. in Computer Science (Pure and Applied Logic), May 2005. Advisor: Prof. Frank Pfenning. Thesis Title: Practical Refinement-Type Checking. Thesis Committee: Frank Pfenning, Bob Harper, Peter Lee, John Reynolds, Alex Aiken (Stanford). Abstract: Software development is a complex and error prone task. Programming languages with strong static type systems assist programmers by capturing and checking the fundamental structure of programs in a very intuitive way. Given this success, it is natural to ask: can we capture and check more of the structure of programs? In this dissertation I describe an approach called refinement-type checking that allows many common program properties to be captured and checked. This approach builds on the strength of the type system of a language by adding the ability to specify refinements of each type. Following previous work, I focus on refinements that include subtyping and a form of intersection types. Central to my approach is the use of a bidirectional checking algorithm. This does not attempt to infer refinements for some expressions, such as functions, but only checks them against refinements. This avoids some difficulties encountered in previous work, and requires that the programmer annotate their program with some of the intended refinements. The required annotations appear to be very reasonable. Further, they document properties in a way that is natural, precise, easy to read, and reliable. I demonstrate the practicality of my approach by showing that it can be used to design a refinement-type checker for a widely-used language with a strong type system: Standard ML. This requires two main technical developments. Firstly, I present a new variant of intersection types that obtain soundness in the presence of call-by-value effects by incorporating a value restriction. Secondly, I present a practical approach to incorporating recursive refinements of ML datatypes, including a pragmatic method for checking the sequential pattern matching construct of ML. I conclude by reporting the results of experiments with my implementation of refinement-type checking for SML. These indicate that refinement-type checking is a practical method for capturing and checking properties of real code. |
||||
| 1988-1990, 1992 |
|
Perth, Australia
|
||
| B.C.M. with First Class
Honours in Computer Science and Pure Mathematics, December 1992. Honours Dissertation Title: Graph Domination, Tabu Search and the Football Pool Problem. Obtained straight A+ results (aside from a single A). The degree B.C.M. (Bachelor of Computer and Mathematical Sciences) is a specialized degree similar to a B.Sc. Conducted research with Gordon Royle of the Computer Science Department in the area of algorithmic combinatorics and optimization, and wrote an 80 page honours dissertation. Hired as a research assistant by the Computer Science department to continue this work, which eventually led to a journal paper that appeared in Discrete Applied Mathematics.
|
||||
| Research Experience | ||||
| 2001-2006 |
|
Perth, Australia
|
||
Continued and extended my thesis work on practical refinement-type checking,
including the following.
| ||||
| 1993-2001 |
|
Pittsburgh, PA, USA
|
||
|
Designed, implemented, and formally proved the correctness of a new approach to
automatically checking properties of programs called refinement-type checking. The
resulting system allows a programmer to declare the intended invariants of their program
in a very natural and convenient way, and obtain automatic feedback when these
invariants are potentially violated by the code of the program. The approach extends
the standard concept of compile-time type checking to allow more of the structure of
programs, including detailed program properties, to be captured and checked. The design
of refinement-type checking is based on a new bidirectional checking algorithm. It also
required the development of a new form of intersection types which are appropriate for
languages that include call-by-value effects. The implemented refinement-type
checker checks programs written using the full Standard ML programming language
(including modules). Some relatively large experiments with programming using this
system have indicated the practicality and usefulness of the approach.
This project began as my thesis work, advised by Frank Pfenning.
Discovered a link between modal and temporal logics and programming languages with a concept of computation stages. This link is based on the much studied Curry-Howard isomorphism between logics and languages. Demonstrated this link formally, and proposed a new type of staged language based on this link, which is appropriate for run-time code generation as well as other instances of staged computation. A concrete language based on this idea, called PML, was implemented at CMU, and a number of other languages based on this idea have been designed elsewhere, most notably the MetaOCaml language which has a reasonably sized user base. Discovered a link between a modal logic with necessity and
possibility and languages with both imperative features and
functions. This builds on work by others which relates lax logic
to the monadic metalanguage, which is a language based on category
theory which also combines imperative features and functions.
Some preliminary work with Frank Pfenning and Bob Harper suggests that
combining this idea with refinement types leads to a practical system
for expressing and checking imperative properties of programs. |
||||
| June-August 1996 |
|
Palo Alto, CA, USA
|
||
| Summer internship working on a web-oriented language with Luca Cardelli. Concentrated on two aspects of the web, namely unreliability and delays in communication. Implemented an interpreter for the language in Java, and presented a paper describing the results at the 1997 USENIX Conference on Domain Specific Languages. This work formed part of the basis for the language WebL, which has been released to the public, and is becoming increasingly popular. | ||||
| June-August 1995 |
|
Aarhus, Denmark
|
||
| Summer internship with BRICS (Basic Research in Computer Science). Investigated multiple execution phases in partial evaluation with Olivier Danvy and developed a relationship between binding-time analysis and temporal logic. Also worked on the Mona project with Nils Klarlund, optimizing an implementation of an efficient decision procedure for second-order monadic logic, using binary decision diagrams to represent automata. | ||||
| June-August 1994 |
|
Rocquencourt, France
|
||
| Summer internship working with Didier Rémy on the design and implementation of an extension to Caml-light with built-in objects and top-level classes. This work was the basis for the design of the object system of the now popular language Objective Caml. | ||||
| 1992 |
|
Perth, Australia
|
||
| Research project in combinatorial
optimization as main assessment for honours year, advised by Gordon
Royle. The main result was better solutions to the much studied
"Football Pool Problem". These solutions were obtained using a
particularly efficient search method combined with some combinatorial
constructions. Employed as a research assistant during the
following summer to continue that research. This work was
published in the journal Discrete Applied Mathematics. Teaching Experience |
||||
| 2001-2006 |
|
Perth, Australia
|
||
Commenced employment in April 2001 as an associate lecturer. Taught the
following.
| ||||
| January-May 1996 |
|
Pittsburgh, PA, USA
|
||
| Teaching assistant for the undergraduate class Fundamental Structures of Computer Science II, assisting Professors Robert Harper and Daniel Jackson. Taught weekly recitation sections, formulated assignments and exams, supervised assignment grading staff, graded exams, and assisted students during weekly office hours. I received an overall score of 4.0 out of 5 from my students in a teaching evaluation. | ||||
| Sept.-Dec. 1994 |
|
Pittsburgh, PA, USA
|
||
| Teaching assistant for the
undergraduate class Problem Solving, assisting Professor
Daniel Slater. Graded assignments, assisted students during
weekly office hours, assisted in choosing problems for the course, and
assisted during lectures. Other Experience |
||||
| 1987-1993 |
Perth, Australia
|
|||
| Worked as a computer and
mathematics consultant during my undergraduate study. In 1991 I
consulted full time. Worked extensively with Unix, PCs, C, SQL,
and Fortran, building software for both scientific and database
applications. I also managed a limited liability company as a
vehicle for consulting.
Completed a number of projects as a consultant. Was a
co-leader in the development of software for libraries, including
cataloging and online search facilities, in which I performed design,
programming, system administration, marketing and customer support
tasks, as well as supervising three other programmers.
Developed data handling software for the West Australian Crime Research
Centre. Extended and enhanced software for tidal research and for
producing official tide prediction tables. Built a package for
performing surveying calculations and storing survey data, which has
been used for over ten years. Finally, based on my honours
research work, I built an engine for finding very good solutions to a
large class of complex optimization problems, and then applied it to
the problem of school timetabling which has since prevented many weeks
of tedious work at a number of high schools. |
||||
Refereed
Publications
Moderator of the newsgroup comp.lang.ml and maintainer of the "Frequently Asked Questions" for the programming language ML, from 1995 to 1999. Program Committee Member: Workshop on Semantics,
Applications and Implementation of Program Generation (SAIG'00),
Montreal, Canada, September 2000. International Conference on Generative
Programming and Component Engineering (GPCE'03), Erfurt, Germany,
September 2003.
MetaOCaml Workshop 2004.
MetaOCaml Workshop 2005.
Computing: The Australasian Theory Symposium (CATS'07).
Served as Referee For (conferences): Dagstuhl
Partial Evaluation Seminar (1996), International Conference on
Functional Programming (1996, 1998), European Symposium on
Programming (1998,2006), Procomet (1998), Typed Lambda
Calculus and Applications (1998), International Conference on
Principles and Practice of Declarative Programming (1999, 2006), Asian
Computer Science (1999), Logic in Computer Science (2000, 2005, 2006 [2]),
Foundations of Software Technology and Theoretical Computer Science (2005 [2]),
Rewriting Techniques and Applications (2005),
Principles of Programming Languages (2006),
Types (2006).
|
||||
| Prof. Frank
Pfenning School of Computer Science Carnegie Mellon University 5000 Forbes Avenue Pittsburgh PA 15213-3891 USA Email: fp@cs.cmu.edu Phone: +1 (412) 268 6343 Fax: +1 (412) 268 5576 |
Dr. Luca Cardelli Microsoft Research 1 Guildhall Street Cambridge CB2 3NH UK Email: luca@luca.demon.co.uk Phone: +44 1223 744 753 Fax: +44 1223 744 777 |
Assoc. Prof.
Olivier Danvy Department of Computer Science University of Aarhus Building 540, Ny Munkegade DK-8000 Aarhus C DENMARK Email: danvy@brics.dk Phone: +45 89 42 33 69 Fax: +45 89 42 32 55 |
||