Rowan Davies: Paper Abstracts
------------------------------------------------------------------
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] and [US.ps.gz].
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.
------------------------------------------------------------------
Practical Refinement-Type Checking
Refinement types allow many more properties of programs to be
expressed and statically checked than conventional type systems. We
present a practical algorithm for refinement-type checking in a lambda
calculus enriched with refinement-type annotations. We prove that our
basic algorithm is sound and complete, and show that every term which
has a refinement type can be annotated as required by our algorithm.
Our positive experience with an implementation of an extension of this
algorithm to the full core language of Standard ML demonstrates that
refinement types can be a practical program development tool in a
realistic programming language. The required refinement type
definitions and annotations are not much of a burden and serve as
formal, machine-checked explanations of code invariants which
otherwise would remain implicit.
Available as [US.ps] and [US.ps.gz].
Some examples of programming with refinement-types in ML are also
available.
Rowan Davies and Frank Pfenning. Practical Refinement-Type
Checking. July 1997. Unpublished draft.
------------------------------------------------------------------
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 for a refinement-type checker for the
core of language of Standard ML, including an introductory example. A
system demonstration will be given at AMAST'97.
Available as [US.ps] and [US.ps.gz].
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. To appear.
------------------------------------------------------------------
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] and [US.ps.gz].
Luca Cardelli and Rowan Davies. Service Combinators for Web
Computing. A version will appear in 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] and [US.ps.gz].
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.
------------------------------------------------------------------
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] and [US.ps.gz].
Philip Wickline, Peter Lee, Frank Pfenning and Rowan Davies.
Modal Types as Staging Specifications for Run-time Code Generation,
ACM Surveys: Special Issue on Partial Evaluation, (to appear 1998).
------------------------------------------------------------------
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 [US.ps] and [US.ps.gz].
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 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] and [US.ps.gz].
Rowan Davies and Gordon Royle. Graph domination, tabu search and the
football pool problem, Discrete Applied Mathematics 74(3):217-228,
1997.
------------------------------------------------------------------