The semantics group meeting in Cachan

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

Dear Semanticists,

A (relatively) brief meeting of the CoFI semantics task group took
place in Cachan --- many thanks to Michel Bidoit for the smooth local
organisation of the entire series of CoFI meetings that set the frame
for this one as well.

Below are the minutes of the meeting, efficiently prepared by Don
Sannella (thanks!).

Just to point out: the immediate task is to prepare the very final
version of the semantics for CASL v.1.0! The authors of the semantics
are working on this hard, and we will be asking others to have a look
through the result soon.

With best regards,

Andrzej Tarlecki

==============================================================================
Semantics Task Group meeting
Cachan, 7 November 1998

Present: Andrzej Tarlecki (chair), Bernd Krieg-Brueckner, Don
Sannella, Pippo Scollo, Michel Bidoit, Maura Cerioli, Anne Haxthausen, 
Sasha Zamulin, Hubert Baumeister, Till Mossakowski

1. Status of semantics: Version 0.9 of the semantics of CASL v1.0 is
ready.  The semantics of structured specs and architectural specs is
basically done but some polishing remains to be done.  For the
semantics of the other parts (basic specs, subsorts, libraries), the
polishing has largely been done already.  Some checking that the parts 
are consistent with each other remains to be done.

2. Completion of semantics: The semantics document will be completed
and checked according to the following schedule:

By end of November: authors to check that their part fits with the
other parts and make these and other final changes, then kibitzing to
take place.

By 15 December: Authors to make changes required as a result of
comments from kibitzers and other authors.

Thereafter: "External" people (Zamulin, Scollo, perhaps Uwe Wolter?)
to check that the document is correct and readable, with feedback to
authors.

3. What next?

Here are some things that should be done by the semantics group:

a. Making the semantics fully institution independent and showing how
   such a semantics instantiates to give full CASL

b. Proving meta-properties of the semantics, including:
   - check the "pre/post-conditions" on the rules
   - check that the static semantics is decidable, perhaps even that
     it has polynomial-time complexity
   - check that the model semantics of a phrase is defined whenever
     its static semantics is successful and "proof obligations"
     (e.g. that fitting morphisms are indeed specification morphisms)
     hold.

c. Extract "proof obligations" in a syntactic form, making them
   explicit in a form that can be checked by tools.  It isn't clear to 
   what extent that this can be done using CASL syntax and/or
   entailment between CASL specifications; if not then we could try to
   give CASL-expressible sufficient conditions.

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

e. Sublanguages of CASL and simplification of semantics for these
   (this is to be kept in mind, but work to be driven by what
   sublanguages are invented by the language design group)

f. Same, but for extensions of CASL

4. What about polishing the semantics, removing the language summary
text and adding other text to make it self-contained?

Opinions differed on the desirability of doing this.  Some (e.g. Bernd)
felt that the semantics is best left as annotations on the language
summary; others (e.g. Andrzej) thought that at least some bits of the
language summary could be deleted, such as concrete syntax; others
(e.g. Don) felt that a separate document would be preferable.

The decision was to leave at it is for now and check with Peter Mosses 
concerning his plans for publishing the Language Summary.

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