No Subject

[Helene Kirchner <Helene.Kirchner@loria.fr>]

From: Helene.Kirchner@loria.fr
To: cofi-tools@brics.dk 
Subject: Minutes of the Bremen meeting

TOOLS task group Meeting

Bremen, September 10-11, 2000

Participants:

Agnes Arnould
Serge Autexier
Helene Kirchner 
Bernd Krieg-Brueckner
Frank Ledoux
Christoph Lueth
Till Mossakowski
Mark van den Brand

AGENDA:

- ATerms versus XML
- Parsers
- Static analysis
- Theorem provers
- Rewriting tools
- Integration of tools

We discussed XML versus ATerm as low-level interchange format.
Textual sharing is available for ATerms, in the last version of the
Aterm library on the web. 
The algorithm for building maximal sharing devised at Amsterdam
for ATerms will be reused for XML.
XML should be adopted as CASL  external format  for communication.
Both ATerms and XML are maintained currently as internal representation
for tools.

Mark van den Brand commits to improve the Amsterdam parser to handle
the full CASL grammar.
On the other hand, another grammar for a Yacc parser has been designed 
for the parser developed by Frederic Voisin. The number of conflicts
is quite good (11), However it is mandatory 
to generate the same abstract syntax tree as is currently done.

More examples/tests are yet needed and there should be a test repository
should be maintained on the Web.

Concerning static analysis, two problems are mentionned:

- The symbol map analysis used in instantiations and views is quite 
inefficient. A more precise note and propositions for solutions
are to be sent by Till to the language design group.

- The model amalgamation property requires to extend the notion of
signature category with subsorts as ...
Currently there is a correct but incomplete algorithm to ensure the 
amalgamation property in presence of subsorting.
A more precise note and propositions for solutions
are to be sent by Till to the semantics group.

In addition Bartek Klin, who is now in Aarhus, is going to work more on
these two problems.

Serge Autexier presented the integration of CATS and INKA through MathWeb
incuding the development graph. He is currently working on the new version of
INKA. 
Further project is to get a version of the environment with Isabelle
(also the new version).
Next step is to add a data base manager (MBase)  and a version manager.


Till Mossakowski presented the HOL-CASL system.
Next projects are
to have more Isabelle tactics available, automatic rewriting,
to be able to prove intended consequences and proof obligations on 
basic data types.

Helene Kirchner presented the integration of ELAN with CASL.
The class of CASL specifications that can be currently executed is the
class of many-sorted conditional equational specifications.
This excludes subsorts and partial functions.
Since WADT'99, the improvements are that specifications can have
mixfix operators, predicates, importations.

The problem of rewriting in theories with subsorts is addressed.  The
set of extended axioms generated by CATS to deal with partiality and
subsorting is not confluent.  Several options are proposed.  Serge
Autexier proposed to use the INKA system and the technique of rippling
to apply the axioms.

Integration of tools.
Three platforms of integration are currently investigated:
- Mathweb at Saarbruecken. The development graph manager could in the future 
evolve towards a developer manager.
- Workbench in Bremen. 
- Toolbus in Amsterdam, which strongly relies on ATerm format.


Priorities for the future work are as follows:

1. (Strongest priority)
For CATS : a complete parser for the current grammar (Mark)
static analysis (Bartek)
Better library management (Till)
ELAN for many-sorted spec and for AC-rewriting  as an oracle in Isabelle
INKA (old version) for order-sorted rewriting

2. 
Structure editor for CASL (Mark)
Isabelle integration with the development graph
new INKA integration with the development graph

3.
Data base management (repository)
Version manager

4.
One integration platform.

=======================================================================