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 [US.ps]
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,
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 [US.ps]
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 [US.ps]
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 [US.ps]
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 [US.ps]
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
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 [US.ps]
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 [US.ps]
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.
The above is a technical report version that is similar to the journal version,
which appeared as follows.
An earlier conference version is also available, but is significantly
shorter, and lacks some important technical material.
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 [US.ps]
Rowan Davies and Gordon
Royle. Graph domination, tabu search and the football pool problem,
Applied Mathematics 74(3):217-228, 1997.