**Achievements **

Extensive work has been made in a number of areas, and we refer to the detailed progress reports from the sites of the WG. We will here just, rather randomly, mention a few of the results during this third year.

- PROGRAMMING. In Munich they have significantly extended their formalization of both Java and the Java Virtual Machine. It now includes a type safety proof for the bytecode verifier, a correctness proof for a simple compiler, and a Hoare logic. At INRIA Rocquencourt, a tactic has been developed for generating proof obligations for imperative program. Also a proof in Coq has been given for safety of a distributed garbage collector.
- COMPUTER ALGEBRA. At INRIA Sophia-Antipolis and Chalmers, various algorithms used in Computer Algebra have been developed and verified in Coq and Agda.
- MATHEMATICS. At Nijmegen, work has been made on formalization of mathematics in proof assistants (notably in Coq). In particular, they are working on the formalization of constructive analysis towards the Fundamental Theorem of Algebra. At INRIA Sophia-Antipolis, Coq has been used in algebra and topology.
- LINGUISTICS. At XRCE (Xerox Research Centre Europe) and at Chalmers, a Grammatical Framework (GF) has been developed. In GF, the user edits interactively a proof, from which a text can be generated text in different natural languages. It is also possible to parse natural languages.
- FORMAL METHODS. At INRIA Sophia-Antipolis experiments have been made to use Coq for industrial problems previously solved by the B method.
- COMPUTATIONAL INTEREPRETATIONS OF CLASSICAL LOGIC. At Paris 7 they have investigated how proofs, even in classical set theory (ZF), can be interpreted as imperative programs.

The proceedings from the second main workshop of the WG, at Kloster Irsee in Germany, has now been published by Springer (LNCS 1657).

**Workshops**

The main workshop of the third year of the working group was organised by the Göteborg site. It was held at the conference centre Lökeberg some 40 km north of Göteborg. It was a very intense meeting with no less than 36 talks and 2 demo sessions. In spite of the high number of participants, 90, the meeting had the atmosphere of a workshop; the reason being the homogeneity of the subject. As for the two previous yearly meetings, the proceedings will be published by Springer in the series "Lecture Notes in Computer Science".

In Göteborg, 27 - 28 March 1999 a Workshop on Dependent Types in Programming, organised together with APPSEM. It had 47 participants from both Working Groups.

**Summer School**

At Giens in the south of France, August 30 - September 10, a
summer school
was organized by
INRIA at Sophia-Antipolis. This two weeks course was for postgraduate
students, researchers and industrials who want to learn about
interactive proof development. There were introductory and
advanced lectures on lambda calculus, type theory, logical frameworks,
program extraction, and other topics which give relevant theoretical
background. Several talks were devoted to applications.
Participants got extensive opportunities to use the systems in a
workstation environment for developing their own proofs.
Among the 55 participants there were 34 PhD students, 14 researchers,
and 7 engineers.

**Visits between the sites**

The main activities of the WG have been the workshops, but there have also been many (around 30) short visits between the sites.