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. ------------------------------------------------------------------