Minutes of the Bonas meeting

[Helene.Kirchner@loria.fr]

(Sorry, I do not have the list of participants)
This was a brief meeting after lunch, mainly to see what are the
progresses made since the Amsterdam meeting and to state some
points to work on.

I. What is new?

- Revision of the formatting package by Peter Mosses, now
including hyperlatex.

- A structure editor is available for CASL via ASF+SDF2. A little more 
work is needed to make it stand-alone, i.e. independent from the 
Tool Bus.

- Repository of parsed specifications: 
one is available in Amsterdam.
Basic data types also provide examples of parsed specifications 
in Bremen. They should be merged at some point.

- Prototyping simple CASL specifications with ELAN.
A note is written and is going to be announced.
The prototype currently handles basic specifications with associative
commutative prefix operators and conditional equations oriented from left
to right.

- In the HOL-CASL environment, a tool is provided to produce a LaTeX
file for a CASL specification text.
Static semantic analysis is available for structured specifications

- Proofs on CASL specifications using PVS. An experiment was done in 
Edimburgh and reported at the WADT workshop.

- A new version for the Web pages for Tools is available and can be
accessed at 
http://www.loria.fr/~hkirchne/CoFI/Tools


II. What to do next ?

- Provide an Emacs mode (no volunteer yet!)

- Parsers:
We need to make a rigorous comparison between the parsers
and compare the outputs. An external person to the group of 
parser designer would be the best option. Is there a volunteer?

Members are encouraged to test all three parsers (Paris, Amsterdam, Bremen)
and to report on divergences.

- Annotations and comments (see Axel Schairer's note):
how to handle them in parsers and other tools. This is also a language 
design issue. Bremen commits to produce comments on this problem.

- Rewrite Engine:
The first prototype is expected to be available soon.
Nancy will work on enlarging the class of CASL specifications executable
by the ELAN rewrite engine.

- Proof environment:
Saarbruecken and Bremen will work on the proof development graph.

- Tools integration:
Bremen will study the workbench idea on special cases.
Alternatives need to be studied as well.

The architecture implemented in HOL-CASL could be opened 
to include external tools, in particular
rewrite engines and theorem provers.


III. Next meeting 

There seems to be interest to organise a meeting in winter 
or spring 1999/2000 either in Genova in connection with
other CoFI groups meetings, or in Nancy.