Rowan Davies: Paper Abstracts

Intersection Types and Computational Effects

We show that standard formulations of intersection type systems are unsound in the presence of computational effects, and propose a solution similar to the value restriction for polymorphism adopted in the revised definition of Standard ML.  It differs in that it is not tied to let-expressions and requires an additional weakening of the usual subtyping rules.  We also present a bi-directional type-checking algorithm for the resulting language that does not require an excessive amount of type annotations and illustrate it through some examples.  We further show that the type assignment system can be extended to incorporate parametric polymorphism.  Taken together, we see our system and associated type-checking algorithm as a significant step towards the introduction of intersection types into realistic programming languages.  The added expressive power would allow many more properties of programs to be stated by the programmer and statically verified by a compiler.    Available as [] and [].

Rowan Davies and Frank Pfenning.  Intersection Types and Computational Effects, March 2000. Revised version to appear in Proceedings of the International Conference on Functional Programming (ICFP'2000), Montreal, Canada, September 2000.

A Judgmental Reconstruction of Modal Logic

We reconsider the foundations of modal logic, following Martin-Loef's  methodology of distinguishing judgments from propositions.  We give constructive meaning explanations for necessity and possibility which yields a simple and uniform system of natural deduction for intuitionistic modal logic which does not exhibit anomalies found in other proposals.  We also give a new presentation of lax logic and find that the lax modality is already expressible using possibility and necessity.  Through a computational interpretation of proofs in modal logic we further obtain a new formulation of Moggi's monadic metalanguage.  Available as [] and [].

Frank Pfenning and Rowan Davies. A Judgmental Reconstruction of Modal Logic, Mathematical Structures in Computer Science. To appear. Notes for an invited talk by Frank Pfenning at the Workshop on Intuitionistic Modal Logics and Applications (IMLA'99), Trento, Italy, July 1999.

Modal Types as Staging Specifications for Run-time Code Generation

This is a short survey of work on languages which incorporate run-time code generation via a type operator based on the necessity operator of modal logic. Available as [] and [].

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

Thesis Proposal: Practical Refinement-Type Checking

One of the major benefits of statically-typed programming languages is that they significantly improve programmer productivity. An obvious reason for this is that they dramatically reduce the amount of time spent debugging by catching most common errors at compile time. A perhaps more important reason is that programmers can use the types to guide understanding of the structure of a piece of code, both during the development of the code, and during code maintenance. One proposal for increasing these benefits is to extend an existing statically-typed language so that each ordinary type is refined by a number of refinement-types, which allow many common program invariants to be expressed and checked. In the resulting system a part of a program which is assigned a particular type may also be assigned multiple refinements of that type. Previous work indicates that automatically inferring refinement-types is algorithmically impractical in general. However, if a programmer annotates their program with enough of the intended refinement-types the problem of checking the annotated program has been found to be much easier in some preliminary experiments.The goal of this work is to demonstrate that refinement-type checking can be a practical and useful addition to a real programming language. To achieve this I intend to design an extension of Standard ML which is suitable for refinement-type checking, extend a real compiler with an efficient refinement-type checker, and demonstrate that this allows many common program invariants to be captured in a practical way.Available as [] and [].

 Some examples of programming with refinement-types in ML are also available.

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

A Practical Refinement-Type Checker for Standard ML

Refinement types allow many more properties of programs to be expressed and statically checked than conventional type systems. This a two-page system description of a refinement-type checker for the core language of Standard ML. It includes an introductory example. A system demonstration was be presented at AMAST'97.  Available as [] and [].

 Some examples of programming with refinement-types in ML are also available.

Rowan Davies. A Practical Refinement-Type Checker for Standard ML, Sixth International Conference on Algebraic Methodology and Software Technology, December 1997. 

Service Combinators for Web Computing

The World-Wide Web is rich in content and services, but access to these resources must be obtained mostly through manual browsers. We would like to be able to write programs that reproduce human browsing behavior, including reactions to slow transmission-rates and failures on many simultaneous links. We thus introduce a concurrent model that directly incorporates the notions of failure and rate of communication, and then describe programming constructs based on this model. Available as [] and [].

Luca Cardelli and Rowan Davies. Service Combinators for Web Computing, IEEE Transactions on Software Engineering 25(3), May/June 1999.  A version appeared at the USENIX Conference on Domain-Specific Languages, Santa Barbara, California, October, 1997. Another version appears as Research Report 148, Digital Equipment Corporation Systems Research Center, Palo Alto, CA, June 1997.

A Temporal-Logic Approach to Binding-Time Analysis

The Curry-Howard isomorphism identifies proofs with typed lambda-calculus terms, and correspondingly identifies propositions with types. We show how this isomorphism can be extended to relate constructive temporal logic with binding-time analysis. In particular, we show how to extend the Curry-Howard isomorphism to include the circle (``next'') operator from linear-time temporal logic. This yields a simply typed temporal lambda-calculus which we prove to be equivalent to a multi-level binding-time analysis like those used in partial evaluation for functional programming languages. Further, we prove that normalization in this calculus can be done in an order corresponding to the times in the logic, which explains why it is relevant to partial evaluation. We then extend this calculus to a small functional language, and give an operational semantics for it. Finally, we prove that this operational semantics correctly reflects the binding-times in the language, a theorem which is the functional programming analog of time-ordered normalization.

 Available as [] and [].

Rowan Davies. A Temporal Logic Approach to Binding-Time Analysis, In E. Clarke, editor, Proceedings of the Eleventh Annual Symposium on Logic in Computer Science, pages 184-195, July 1996. 

A Modal Analysis of Staged Computation

We show that a type system based on the intuitionistic modal logic S4 provides an expressive framework for specifying and analyzing computation stages in the context of functional languages. Our main technical result is a conservative embedding of Nielson and Nielson's two-level functional language in our language, thus proving that binding-time correctness is equivalent to modal correctness on this fragment. In addition our language can also express immediate evaluation and sharing of code across multiple stages, thus supporting run-time code generation as well as partial evaluation. Available as [] and [US.pdf].

The above is a technical report version that is similar to the journal version, which appeared as follows.

  • Rowan Davies and Frank Pfenning.  A Modal Analysis of Staged Computation, Journal of the ACM, 48(3):555-604, 2001.
  • An earlier conference version is also available, but is significantly shorter, and lacks some important technical material.

  • Rowan Davies and Frank Pfenning A Modal Analysis of Staged Computation, 23rd Annual ACM Symposium on Principles of Programming Languages (POPL'96), pages 258-270, January 1996.
  • An even earlier version was presented at the workshop on Types for Program Analysis, Aarhus, Denmark, May 1995.

    Graph Domination, Tabu Search and the Football Pool Problem

    We describe the use of a tabu search algorithm for generating near minimum dominating sets in graphs. We demonstrate the effectiveness of this algorithm by considering a previously studied class of graphs, the so-called "football pool" graphs, and improving many of the known upper bounds for this class.  Available as [] and [].

    Rowan Davies and Gordon Royle. Graph domination, tabu search and the football pool problem, Discrete Applied Mathematics 74(3):217-228, 1997. Home page