Minutes of the Amsterdam meeting

["Andrzej Tarlecki" <tarlecki@mimuw.edu.pl>]

Dear Semanticists,

A brief and somewhat informal meeting of the CoFI semantics task group
took place in Amsterdam, on Friday, March 26th, evening, as a prelude
to the CoFI workshop organized there on the following Saturday and
Sunday (Many thanks to Mark van den Brand for the local organization!)

Below are the minutes, taken by Maura Cerioli and typed in by me
(actually, I typed them a while ago, but it seems that I have managed
not to send them out then ---- sorry).

With best regards,

Andrzej Tarlecki

==============================================================================
Semantics Task Group meeting
Amsterdam, 26 March 1999

Present: Andrzej Tarlecki (chair), Hubert Baumeister (arriving late :-),
Michel Bidoit (calling himself an observer), Maura Cerioli, Till
Mossakowski, Peter Mosses, Don Sannella.

1. Status of the semantics:

Version 0.95 of the semantics of CASL v1.0 is ready (as announced
earlier). Although no major changes are expected anymore, some final
polishing is required. It is now the time for kibitzers to really step
in and go through the parts of the semantics assigned to them to help
the authors to finalize their parts. It was also agreed that all the
authors should go through the whole semantics to check for consistency
with their parts.  May 6th was set as a deadline for sending the final
versions of each part of the semantics to Don Sannella.

1a. The issue of constraints on the names used in the free data type
construct was discussed: a recommendation was made to the language
design group for a further restriction to exclude also re-use of sort
names and constructor and selector names in this construct.

2. Plans for publishing the semantics:

The semantics should be published. The form of publication was
discussed, in particular whether the current form (with semantics
inserted into the text of the summary) should be kept. While this was
considered possible and valuable for some WWW version of the
semantics, it was also said that the summary should be published
without the technicalities of the semantics discouraging many readers
from looking through it. Consequently, a version of the semantics
document without the full summary included is to be developed.
However, some explanation and concepts from the summary would have to
be retained. The result could be published in some volume together
with the summary, or as an appendix to the summary.

3. Plans for further work:

Not much new was discussed here w.r.t. the minutes of the previous
meeting (Cachan, November 7th):

a. Making the semantics fully institution independent and showing how
   such a semantics instantiates to give full CASL.
   The structured specifications part is already in the appropriate
   form. Architectural specifications is to be completed in a similar
   style. Depending on the feasibility of such a potentially major
   rewrite of this part of the semantics, it might be even possible to do
   this for the next version of the semantics.

b. Proving meta-properties of the semantics.

c. Extract "proof obligations" in a syntactic form.

d. Proof systems for: basic specs, structured specs, entailment
   between specs.

e. Sublanguages and extensions of CASL and modification of semantics
   for these.

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