Minutes of the Berlin meeting

[Helene.Kirchner@loria.fr]

TOOLS Group Meeting in Berlin (ETAPS'2000)

Participants: (no order)
Helene Kirchner
Mark Van den Brand
Bernd Krieg-Bruechner
David Aspinau
Bartek Klin
Agnes Arnould
Hubert Baumeister
Serge Autexier
Giuseppe Scollo
Norman Pagel
Nikos Mylonakis
Markus Roggenbach
Till Mossakowski
Michel Bidoit
Andrzej Tarlecki 


Saturday April 1

Reports of the sites

Bremen: Presentation of the CASL Tool Set 
by Till Mossakowski
The CASL tool set is a set of tools for
parsing, static analysis, locical encoding and formatting
of CASL specifications. It is being developed as a joint
effort between different sites (Bremen, Warsaw, Amsterdam, Orsay,
Saarbruecken).
Recent progress involve:
- Integration of the parser of Frederic Voisin
- Static analysis for basic and structured specifications
- Visualisation of the dependency graph of specifications
- Improvement of the LaTeX output
- Proofs by induction via Isabelle.

Saarbruecken: CASL-INKA interface
by Serge Autexier
- The development graph for INKA specifications is adapted 
to CASL structured specifications.
It will be soon available in the CASL tool set.

Nancy
by Helene Kirchner
Executing CASL Equational Specifications 
with the ELAN Rewrite Engine
We are currently working on the following extension of the prototype
presented at Bonas:: 
- Mixfix operators (possibly Associative-Commutative) 
- Structured specifications
- Handling predicate declarations



Sunday April 2

- OpenMath and CASL
by Michael Kohlhase
Presentation of the OpenMath initiative and of the 
OMDoc project for including specifications into OpenMath.
The OpenMath initiative tries to standardize a format for symbolic
computer algebra. However, the standard is still without a clear
semantics, and here is the point where a link between this community
and the CASL community could be very fruitful.
Moreover, the OMDOC format (based on XML) and the MBase theorem database
system is in itself interesting.
Bremen is currently developing a translation
from CASL to OMDOC (in cooperation with Michael Kohlhase).

- Comparison between ATerms and XML 
The following question was debatted:
Is it sensible to consider the replacement of ATerm format by XML?
The conclusion was that more insight is needed. Different solutions are possible.
It is too early to reconsider ATerm as an exchange format for our internal 
tools, but a translation from ATerm format to XML is strongly suitable.

- Comments and annotations
The proposal by Bernd and Peter on the place of comments in specifications
is approved.
The problem of nested comments has to be checked.
A migration tool for changing annotations in already written CASL 
specifications should be provided.
The CASL style file has also to be changed.
For annotations, the proposal is similar to comments.

- Reports on parsers
A tool for automatically computing the differences between two
abstract syntax trees generated by different parsers is going to be
produced by Mark van den Brand and Frederic Voisin.
Still  some work is needed on improving the Bremen parser.

- Integration:
There is a concensus on the following decision: until december, our 
efforts will concentrate on integrating tools from the different groups
into the set of tools initiated in Bremen. 
The architecture of this set of tools should be:
   - modular and composed of:
           minimal set for writing and parsing CASL specifications, 
checking  well-formedness, editing them.
           library of basic examples allowing to check the tools
basic data types and exemples from the CASL tutorial and manual
           representation of the development graph (prover independent)
           connection to the Isabelle Prover
           connection to the Inka Prover
           connection to the ELAN evaluator 
   - open and easily incremented by new tools (KIV? OMDOC?)
   - running on possible architectures: PC Linux, SUN Solaris at least.
          

- Web page.
They will be updated to present the CASL Tool Set. For evaluation of a new tool,
it is  suggested that the coordinator designates an evaluator and a deadline
for evaluation, with precise criteria and some tests to run.

- Next meeting:
  - probably a next meeting in september (between 11 and 16)
either in Edinburgh or in Bremen.
  - several visits between sites are planned to make progress on the 
implementation of tools.


Helene Kirchner