Why is it good with a WG for Types?
The subject of the Working Group is computer assisted development of proofs and programs. The group is concerned with questions ranging from foundational theoretical issues to real industrial applications, where the theoretical problem often comes from experience obtained from applications.
To build a computer system which will function as a universal tool for developing theories and proofs, is obviously a long term goal. But its fulfilment can be expected to have far reaching consequences not only for Information Technology, but in many areas where exact and correct reasoning is crucial.
The policy of the last years, both on the European and national levels, to mainly support projects with rather immediate industrial applications make these kind of projects difficult to sustain, although the long term industrial impact might be considerably stronger.
The Working Group is very important for the people working in this field. The meetings that are held within the WG would not have been possible without the economic support from Esprit. And they cannot be replaced by ordinary conferences, which are much less focussed: the meetings of the WG bring together people from different areas (theoretical computer science, implementation, and industry), working towards the same goal.
It is difficult to see how the comparatively small sum of money that a WG receives could be used in a more efficient way to support scientific cooperation on the European level and focus research in an area which is of vital long term importance to industry.
Achievements
Below are detailed progress reports from the sites of the WG. We will here just mention a few of the achievements during this first year.
In France, Coq was used by the G.I.E. Dyade (Bull-INRIA) for developing proofs of cryptographic protocols involved in electronical transactions. Coq is also used by CNET in the validation of algorithms involved in the ATM protocols. Edinburgh has continued its collaboration with Harlequin Ltd on formalizing memory management and correctness of garbage collection. Göteborg has started a cooperation with the company Logikkonsult, which is using formal methods on safety critical systems like rail yards and nuclear power plants.
At Cambridge, a new approach to modelling protocols has been developed, based upon the technique of inductive definitions. Several protocols have been mechanically analysed using the theorem prover Isabelle. Typically, secrecy and authenticity of critical message items can be shown, even in a partially compromised system. One protocol, designed for an industrial application, was found to be faulty but could be verified after correction.
Java-light - a large sequential sublanguage of Java - has been formalized (abstract syntax, type system, well-formedness conditions, and an operational (evaluation) semantics). Based on this formalization, type soundness has been proven. All definitions and proofs have been done formally in the theorem prover Isabelle/HOL. This work has been done by the Munich site.
At Sophia-Antipolis a proof of the correctness of Buchberger's algorithm, which is important in computer algebra, has been developed in the Coq proof assistant. The formulation of the algorithm in Coq can then be efficiently compiled and used for computations.
In Udine they have studied the possibility of proving formally in Coq basic results in the theory of exact computation on real numbers, an area which has received a lot of attention recently. In Padova, Göteborg and Helsinki, formal toplogy is used to develop analysis; in particular, a proof of the Hahn-Banach theorem from functional analysis was developed on the theorem prover Half.
In Helsinki, a grammar of informal mathematical language has been developed. This work has resulted in a Haskell implementation that makes it possible to interact with proof editors in six natural languages. Experimental versions of this interface are being built in collaboration with Göteborg and with Durham. As an example of program development using proof editing in natural language, a natural-language interface to regular expressions has been written. Work on translating formal text of a proof system to natural language is also done in Sophia-Antipolis.
Nine Ph.D. thesis were finished within the WG during the period.
Workshops
The main workshop of the first year of the working group was organised by the Lyon site. It was held at the conference centre of CNRS at Aussois December 15th to 19th, 1996. It was a very intense meeting with no less than 47 talks and 3 demo sessions. In spite of the high number of participants, 94, the meeting had the atmosphere of a workshop; the reason being the homogeneity of the subject. The proceedings will be published by Springer in the series "Lecture Notes in Computer Science"; we expect them to appear early next year.
A smaller workshop was organised by the sub-site at Durham, 30th August to 1st September 1997. The subject was "Subtyping, inheritance and modular development of proofs" which is fundamental for most applications of the proof systems. The meeting had 23 participants and 13 talks were given. The proceedings are published "on-line" on Internet and can be obtained from the home page of the WG.
Visits between the sites
The main activities of the WG have been the workshops, but there have also been a number of short visits between the sites. In particular, there have been several exchanges between Edinburgh, Cambridge and Nijmegen on the one side and Lyon and Rocquencourt on the other. One topic of the visits has been investigating the high-level architecture of theorem provers, which may well lead to standardisation of the proof systems. In long term this is important, although the diversity of theories and implementations is a scientific strength of the WG since it gives multiple experimental platforms.