ESPRIT Working Group Proposal

TYPES

March 18, 1996

1 Summary

The subject of this proposal is computer assisted development of proofs and programs, an area which can be expected to be of vital concern for industry in the future. During the Esprit BRA projects “Logical Frameworks” and “Types for Proofs and Programs” several systems were implemented which are now beginning to be used for applications in computer science, relevant to industry. These projects had eleven main sites in France, Germany, Great Britain, Italy, the Netherlands and Sweden and a unique competence in the area has been built up. There are two purposes of a working group on types. The first is to keep the community together and thereby ensure the continuation and development of our ideas; the second is that it will form a basis for specific Long Term Esprit projects in cooperation with industry.

2 Objectives

The proposed working group is concerned with computer assisted development of proofs and programs. This is an important area because formal proofs can be expected to play a major role in future technology for the design of correct hardware and software. The long-term goal of formally specified and verified hardware and software is of great importance for industry for the economic production of evermore complex and reliable computer systems.

Within the Esprit BRA projects “Logical Frameworks” and “Types for Proofs and Programs,” several proof systems based on type theory have been implemented. They have been used on a number of fairly large examples, ranging from pure mathematics to program development. These projects have received excellent reviews by which the work done within them is considered as the state of the art for interactive proof systems.

Examples of computer systems used in industry and with similar aims as ours are the HOL system and the Boyer-Moore theorem prover; in contrast to our systems, they are not founded on constructive type theory. The advantage of using type theory is that its basic concepts are also fundamental in computer science: proofs in type theory can be viewed as programs and propositions as types. In fact, type theory can be seen as a functional programming language with a very rich type structure. Proof-checking is the same as type-checking which means that the kernel of the proof-checker in a system based on type theory is very simple.

Our proof systems can be seen as universal tools in which different theories can be expressed. The design and implementation of such a system is a major task and we cannot yet claim that they are ready for routine industrial use. We expect to continue with Long Term Esprit projects which will be focussed on e.g. implementation issues and applications of relevance for industry. However, it is of prime importance that this research community is kept together so that it can form a basis for more applied projects; this is one of the main objectives for a working group on types.

In the remainder of this section, we will give a short description of the areas and kinds of problems we expect the working group to address: implementations, application, refinement of formalism, and semantics of type theory. There is a close interaction between these areas; for instance, examples developed in the systems often have important consequences for both the implementations and the formalisms, sometimes resulting in deep theoretical issues.

2.1 Implementation of tools

The implementation of tools for computer aided formal reasoning is one of the focussing points of our work. ALF (Göteborg), Coq (Paris, Lyon), Isabelle (Cambridge) and LEGO (Edinburgh) are used at many places in Europe. We are working on improving our tools, to make them easier to use, increase their flexibility and efficiency and extend their functionality. To maintain and improve the high quality of our tools, interaction and discussions between the different implementers and users are essential. We are also interested in trying to unify our work and to develop a system that could meet industry standard for computer aided formal reasoning. The interaction of the working group in the area of implementations will focus on the following topics:

Design of proof engines. It is essential that the proof engines, which are the heart of our tools, are reliable, robust and reasonably efficient. To achieve our goals we have to interact with researchers outside our field, especially in the area of rewriting and automatic proof search. Other topics include the implementation of explicit substitution and higher order unification which are of importance for systems based on type theory. An important theoretical issue for the proof engines is the relation between various notions of inductive definitions.

Design of user interfaces. The usability of a tool depends a great deal on the quality of the user interface. We are experimenting with window based, point and click interfaces: the CENTAUR system (Sophia-Antipolis) is a general tool which is used by several systems, and more specific window interfaces for ALF and Coq have been developed. We also hope for a mutual fertilisation with program development systems.

Interfaces to other systems and tools. For many real applications it is essential to have interfaces to other computer systems. Automatic theorem provers have already been incorporated in some of the systems, but we believe that our systems now have reached a stage when they could benefit also from integrations with e.g. computer algebra and hardware specification tools.

2.2 Applications

In the languages used in our implementations, it is possible to express programs and specifications and also to interpret proofs as programs. Substantial work has been done in the theory of extracting programs from proofs: for efficiency reasons, it is crucial to remove computationally irrelevant parts of the proofs. Various techniques for this have been developed. The methods developed have been used on a number of examples and we consider program derivation to be an important area for our systems.

In program correctness, we can mention work on protocol verification in Coq done in cooperation with Philips in Eindhoven. Isabelle has also been used for protocol verification, using finite model-checking. In Edinburgh LEGO is used in a joint project with industry for program correctness; e.g. they are verifying a garbage collector for ML. Work is going on in representing process calculi in a uniform way in ALF, and we expect to develop examples from concurrency. Also, work on hardware verification has been started in ALF.

Concerning mathematics, our systems have been particularly successful in the metamathematics of formal systems of importance for computer science; e.g., several proofs of normalization have been done in ALF, Coq and LEGO, and correctness of a type-checking algorithm has been verified in LEGO. Another example, in mathematics relevant for computer science, is a termination proof of term rewriting with the multiset path ordering, developed in Coq. Isabelle has been used for formalizations and equivalence proofs of various programming language semantics.

Relatively little has been done so far in algebra and analysis, partly because of difficulties in finding appropriate ways to represent theories of this kind in type theory. However, examples in Galois theory have been developed in LEGO, formal topology has been implemented in ALF, and a fair portion of category theory has been developed in Coq. We are now beginning to have a better understanding of how to express algebra and analysis and expect interesting examples to be developed in the systems.

Type theory has also been used in linguistics, and in Helsinki the ALF system has been used for several applications. For example, a program has been developed which transforms a type theory proof to ordinary English text.

2.3 Refinement of formalisms

Type theory is a family of evolving formalisms, we are continuously refining the theory and different variants are used at different sites. From a researcher’s point of view this is good: possible alternatives will be explored and hopefully a good solution in terms of simplicity and usability will come out in the end. In the current stage communication between the different sites is essential to keep the discussion going. At the same time we are trying to identify the common ground and maybe define a common language on which we can agree; the development here is similar to the evolution of programming languages.

Here is an incomplete list of topics which are currently discussed in this context.

Modularity and abstraction. Although we share a lot of common problems with programming languages, it is becoming clear that these questions are even harder to solve for languages which include specifications and proofs. On the other hand there is reason to hope that a good solution for type theory will be useful for the design of module systems for programming.

Data types. We are making good progress in this field but there are still some open questions concerning the precise status of pattern matching and the use of infinite (or co-inductive) types like streams. The latter is highly relevant for the design of interactive and concurrent systems.

Subtyping and inheritance. This field is closely related to the general question of modularity and abstraction. In the context of proof systems subtyping is highly relevant for the reuse of proofs and specifications. Moreover, we hope to exploit ideas from object oriented programming and to get a better explanation of inheritance.

Term rewriting. It is still problematic to perform (algebraic) equational reasoning in proof systems. Investigation of extensions of constructive type theory with rewriting techniques will be important to overcome this difficulty.

Extensionality. The apparently abstract question whether one should use an extensional or intensional theory has many practical consequences. A more extensional view of algorithms would improve the re-usability of code but seems harder to implement. However, some progress has been made recently in this field, especially concerning the concepts of quotient types and subset types.

2.4 Semantics of Type Theory

Constructive type theory is a foundational system for constructive mathematics: it provides a language in which mathematics may be formulated, and clarifies the principles that may be used in this formulation. In this way, it plays a similar role as Zermelo-Fraenkel set theory plays for classical mathematics; however, type theory has a detailed meaning explanation, developed by P. Martin-Löf, based on a concrete computational ontology using concepts that are familiar in functional programming, such as data types, the constructors and selectors of data types, computation to canonical form, and (restricted forms of) recursive definition.

It is of great interest to analyse the connections between this formalism and others used in the semantics of programming languages, namely category theory and domain theory. There are many detailed choices to be made in the presentation of a formalism such as type theory, that affect the meta theory and the usability of the formalism: studying the meaning explanation of type theory in relation to other semantic formalisms gives insight into these choices. Work along these lines is currently being done. Carrying out the details of expressing the semantics of type theory in category theory has turned out to be surprisingly difficult, revealing important coherence problems; techniques used in type theory for analysing reductions seem to be a promising way to attack such problems. There has been some work on the semantics of dependent types in domain theory, that has been used in work on partial interpretation. Such a semantics may be important for the work on program extraction from proofs, and gives an elegant way to justify program transformations. It may be possible to use this technique for transformation of proofs as well.

3 Activities

The activities of an Esprit working group fit well with what we see as the purpose of a working group on types: to function as a common ground for our different interests in proof-development systems. So we plan

• one major workshop every year, with a collection of selected, refereed papers published after the workshop,

• one or two small workshops per year on topics of special interest. These are to be attended by researchers working on the topic, and producing informal, un-refereed proceedings of work in progress,

• short visits between the sites by individual researchers.

Our previous workshops have had of about 80 participants each and the smaller between 10 and 30 participants.

4 Information dissemination

We plan to publish the proceedings of the annual workshops in the LNCS series as done previously. The smaller workshops should produce informal proceedings which are published as technical reports of the organising site.

We will exploit the internet as a medium for fast information dissemination even more than before. We plan to organise and layout a system of pages on the WWW which features different entry points so that it can be used by an interested lay person, by researchers in other areas in computer science and by the members of the group itself. These web pages give direct access to the relevant articles and technical reports, to lecture notes and copies of slides, to manuals and to executable copies of our systems.

We plan a summer school, open both to advanced students and industry. There will be lectures as well as ample opportunities to use our systems. In 1993 we held such a summer school in Båstad, Sweden, which had about 60 participants.

5 Management

Since the sites are mainly the same as in the previous Esprit projects on types, this is already a well functioning community with good personal contacts between the key proposers. The working group will be coordinated by Chalmers in Göteborg with Jan Smith as coordinator. There will be a steering committee consisting of three persons which the coordinator will consult in all questions of importance; the members of the committee will be exchanged each year.

Site  Key proposer  Funding
Cambridge  Larry Paulsson  15 kECU
Edinburgh  Rod Burstall  24 kECU
Göteborg  Jan Smith  24 kECU
Helsinki  Jan von Plato  15 kECU
Lyon  Christine Paulin-Mohring 24 kECU
Manchester  Peter Aczel  15 kECU
München  Tobias Nipkow  20 kECU
Nijmegen  Henk Barendregt  20 kECU
Oxford  Lincoln Wallen  20 kECU
Paris 7  Michel Parigot  20 kECU
Rocquencourt  Gilles Dowek  24 kECU
Sophia-Antipolis Joëlle Despeyroux  24 kECU
Torino  Mario Coppo  20 kECU
Udine  Furio Honsell  20 kECU
Utrecht  Marc Bezem  15 kECU

6 Resources

We apply for an average of 20 kECU for each site for 3 years, distributed according to the table above. We estimate the additional cost for the coordinating site to 20 kECU and for the planned summer school to 10 kECU. The total sum we apply for is then 330 kECU.

7 Associated sites

In addition to the main sites there are seven associated sites. They contain persons whom we want to regularly take part in the activities of the working group. They will receive economical support for travels from the site to which they are associated.

Associated site  Key person  Associated to
University of Birmingham  Eike Ritter  Cambridge
University of Darmstadt  Thomas Streicher München
University of Durham  Zhaohui Luo  Edinburgh
University of Oslo  Anne Salvesen  Göteborg
University of Padova  Giovanni Sambin Udine
University of Stockholm Per Martin-Löf Göteborg
Queen Mary College, London David Pym  Oxford