Lisbon meeting -> schedule of work!

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

Dear Semantics People,

Just a few words to report on the meeting of the CoFI semantics group
in Lisbon during ETAPS. Four group members (Till Mossakowski, Peter
Mosses, Don Sannella and Andrzej Tarlecki) and a guest (Bernd
Krieg-Brueckner) were present. We have discussed the schedule of our
further work, some specific technical issues related to the last
minute changes in CASL v.0.99, and the possibility of making the CASL
semantics institution-independent.

Schedule
========

The main goal is to produce semantics for CASL. As you all know, CASL
v.0.99 is to be officially released any minute now, with a hope that
there will be only very minor adjustments (if any at all) to obtain
v.1.0. Therefore, we should aim at producing a complete semantics for
v.0.99 as soon as possible. A rather tight schedule has been agreed
upon in Lisbon; I allow myself to change the dates taking into account
the change of date for the v.0.99 release:

- as soon as v.0.99 is officially released, Don will split the text up
and will send the appropriate chapters to the subgroups responsible
for the semantics of particular parts of the language.

- we give ourselves about three weeks to produce the semantics for
each part; by May 16th each part of the semantics should be sent to
the assigned kibitzers.

- by May 23rd we expect that the semantics of each part will have been
studied and commented upon by the kibitzers.  The authors have a few
days to take these comments into account before sending their parts of
the semantics to Don.

- by May 30th Don will have the whole text integrated.

Let me remind you once more of the assignments:

  Basic specifications: Don (kibitzer Hubert)
  Subsorting: Anne and Maura (kibitzer Till)
  Structured specifications: Till and Hubert (kibitzer Andrzej)
  Architectural specifications: Andrzej (kibitzer Don)
  Libraries: Peter (kibitzer Hans-Joerg)

Thus, by the beginning of June we should have a single document that
consists of the summary of CASL v.0.99 and its semantics, much in the
style of the semantics we had for v.0.97. We expect that this version
is going to be very close to the final language design and semantics
--- therefore we need some external volunteers to look at it at this
stage and comment on the semantics, mainly from the technical point of
view but also with an eye to the style of presentation. One of the
reasons for writing the semantics as comments on the summary is to
allow the consistency of the two descriptions to be checked easily,
and this is also the time to perform this check.

*********************** Volunteers needed!!! *************************

PLEASE, ANYONE WHO WOULD LIKE TO HAVE A CRITICAL LOOK AT THE SEMANTICS
AT THIS STAGE, LET ME KNOW!!!

**********************************************************************

The input and critical comments from the above work on the semantics
should be the major factor to be taken into account in the final CASL
v.1.0 design --- which we expect to be done soon after the semantics
for v.0.99 is ready. Only minor revisions (if any) are expected then,
so it should be easy to adjust the semantics to v.1.0. The main job
then will be to produce a more readable semantics document, with the
same structure but more readable than the full mixture of informal
summary and formal semantics. This should be produced from the
previous version, largely by deleting redundant text.  We agreed that
as before, Don will start by editing his basic specification chapters
to set an example for the style and format of the other parts.

The result should be a single semantics document for CASL v.1.0, to
accompany its more informal summary.

Language design issues
======================

As usual, there was no way to separate semantic discussions from the
language design. We have looked at the changes to the languages design
discussed in Lisbon, and concluded that they pose no major problems
for the semantics. The actual changes will be reflected by the new
version of CASL (v.0.99) to be released about now.

Institution independence
========================

It would be desirable to make the semantics of CASL as institution
independent as possible. This was one of the points that the IFIP
WG1.3 referees stressed. It seems that a notion of institution with
identifiers (proposed by Till, close to that of institution with
syntax of Sannella & Tarlecki'86) should provide an appropriate
abstract framework for this. Most roughly, an institution with
identifiers is an institution additionally equipped with a functor
that extracts from each signature the set of fully qualified
identifiers that occur in it, and with some possibility of lifting a
partial map on such identifiers to a "less partial" map, intuitively
capturing extension of a map on identifiers to compound identifiers.

We agreed that introducing full technicalities in the current
semantics document might be overkill; instead the semantics will be
written as it is, but the actual formal definitions and concepts
should rely only on a limited vocabulary of notions and constructs
that can be defined in an arbitrary institution with identifiers. This
will not affect the basic specifications, subsorting constructs and
libraries at all.

For structured and architectural specifications, Till is to prepare a
vocabulary of concepts to be used (mainly to deal with signatures and
their morphisms: how symbol sets determine subsignatures and how
symbols maps determine signature morphisms --- this has been already
partly smuggled into the current summary v.0.99, except for the part
on compound identifiers). These are defined now specifically for the
institution of CASL. However, they can also be defined in an arbitrary
institution with identifiers, so that other such institutions might be
plugged into CASL structuring and architectural mechanisms in the
future. There should be a separate note presenting the exact
definition of institutions with identifiers and discussing their use
in the definition of CASL, with a pointer to this from the semantics
document.

Wishing everybody good work!

Best regards,

Andrzej Tarlecki