Informal minutes of IFIP Working Group 2.1
58th meeting, Rome, Italy
Monday 2004-01-26 to Friday 2004-01-30

Contents of this page:    Administrative matters  |  Technical presentations
(Last updated 1st April 2004.)


Organizational and administrative matters

List of attendees

Members: Observers:

TC2 papers (Fri 2004-01-30, 09:10)

Before he died, TC2 Chair Armando Haeberer had been planning an initiative to strengthen the links between TC2 working groups; this proposal was discussed at Meeting 56 and Meeting 57.

It still is not clear whether Haeberer's successor as TC2 Chair will continue with this initiative, and it hasn't been mentioned by TC2 recently. Therefore it was decided to postpone any further effort on the project until and and unless someone picks it up again.


Formal invitation letters (Fri 2004-01-30, 10:30)

The secretary omitted to send formal invitation letters to this meeting, as discussed at the last meeting. Once again, this left the meeting starting time vague, and lost the opportunity to stress the importance of attending the whole meeting. (The secretary did, however, remember to send reminders to members and observers who have missed several meetings.)

From Meeting 59, the secretary will send out formal invitations by email, emphasizing the points mentioned above.


Formal resolution (Fri 2004-01-30, 11:05)

On their second pilgrimage to Rome on the occasion of the 58th meeting of WG2.1, the members and the observers present wish to thank Alberto Pettorossi of the University of Rome, Maurizio Proietti of IASI-CNR, and their assistants, for their stellar job in organizing and hosting the meeting.

Notwithstanding our lack of angelic prescience regarding the weather in selecting our venue, we have been warmed by the spiritual context in which the meeting was embedded.

We explored - on multiple levels - the foundations of an elaborate architecture, under the guidance of an ever enthusiastic and energetic host. May this inspire the group in its own quest for the fundamentals of software construction.


Next meetings (Fri 2004-01-30, 11:10)

Meeting 59
This will be organized by Roland Backhouse, near Nottingham, on 6th to 10th September 2004.

Meeting 60
This will be organized by Allen Goldberg, Lambert Meertens and Doug Smith, in Northern California, probably in the week 22nd to 26th May 2005. (That's a Sunday to Thursday; it will make it easier to stay over a Saturday night to get cheaper flights, and it will steer clear of the Memorial Day holiday the following weekend.)

Meeting 61
This will be held somewhere in Europe in early 2006.


Algol Bulletin (Fri 2004-01-30, 09:10)

Brian Wichmann has been working on digitizing back issues of The Algol Bulletin. He is still working on collecting authors' permission to reproduce copyright material; if you can help, please let him or the secretary know. A draft of the archive is available now.

The group would like to express their thanks to Brian Wichmann for carrying out this noble task.



Technical presentations

Note: presentation summaries were prepared by the speakers.


Presentation: Swierstra, Polish parsers, step by step (Mon 2004-01-26, 11:45)

No abstract provided.


Presentation: Hutton, Compiling exceptions correctly (Mon 2004-01-26, 14:10)

Exceptions are an important feature of modern programming languages, but their compilation has traditionally been viewed as an advanced topic. We show that the standard method of compiling exceptions using stack unwinding can in fact be explained and verified both simply and precisely, using elementary functional programming techniques. In particular, we develop a compiler for a small language with exceptions, together with a proof of its correctness.

(The slides and a draft paper are available. This is joint work with Joel Wright.)


Presentation: Hofstedt, Integration of declarative and constraint programming (Mon 2004-01-26, 15:00)

Combining a set of existing constraint solvers into an integrated system of cooperating solvers is a useful and economic principle to solve hybrid constraint problems. We show that this approach can also be used to integrate different language paradigms into a unified framework. Exemplarily, we present the integration of a logic language with constraint systems, and the extension of a functional logic language with constraints.


Presentation: Gibbons, Streaming algorithms (Mon 2004-01-26, 16:00)

Unfolds generate data structures, and folds consume them. A hylomorphism is a fold after an unfold, generating then consuming a virtual data structure. A metamorphism is the opposite composition, an unfold after a fold; typically, it will convert from one data representation to another.

In general, metamorphisms are less interesting than hylomorphisms: there is no automatic fusion to deforest the intermediate virtual data structure. However, under certain conditions fusion is possible: some of the work of the unfold can be done before all of the fold is complete. This permits streaming metamorphisms, and among other things allows conversion of infinite data representations.

We present the theory and outline some examples.

(The slides are available.)


Presentation: Swierstra, Scripting the type inference process (Mon 2004-01-26, 17:10)

No abstract provided.


Presentation: Curtis, Modelling non-determinism (Tue 2004-01-27, 09:00)

A relational model that has recently been proposed for modelling angelic and demonic non-determinism consists of up-closed multirelations. Such specifications can be refined until they contain only one kind of nondetermistic choice. Then they can be translated into programs in which those remaining choices are made interactively by an external agent at run time.

(A draft paper is available. This is joint work with Clare Martin and Ingrid Rewitzky.)


Presentation: Pepper, Transforming LR-grammars into LL-grammars, with a little cheating (Tue 2004-01-27, 10:10)

Top-down parsing based on LL-grammars is easily programmable, while LR-style parsers are usually hard to code. Unfortunaltely, LR grammars are strictly more expressive than LL grammars. We present a formal transformation that allows the conversion of any LR grammar into an equivalent LL grammar. The transformation is easy to comprehend and to verify. Obviously, this cannot be done solely within the realm of context-free grammars. Our solution is to add a little bit of context-sensitivity to the grammar, which is, however, efficiently implementable in (functional) parsers.


Presentation: Cohen, Towards a discipline of cryptographic programming (Tue 2004-01-27, 11:30)

No abstract provided.


Presentation: Möller, Modal Kleene algebra and applications (Wed 2004-01-28, 10:05)

Besides its applications within formal language theory, Kleene algebra supports an abstract treatment of programs and state transition systems. Kozen's Kleene algebra with tests (KAT) has extended this classical framework by an abstract representation of sets of states. Recently, the present author and colleagues (among them Jules Desharnais) have enriched KAT with domain/codomain operations that determine the set of initial/final states of a transition system.

In these modal Kleene algebras one can define image and inverse image and hence the backward and forward diamond and box operators of dynamic logic and similar frameworks. This can be extended to include infinite iteration and hence a simple algebraic description of reactive systems. Other applications are the derivation of Greedy-like algorithms, the analysis of two-person games, questions of termination and confluence and propositional Hoare logic.

See working papers DOM-6, DOM-7, DOM-8, DOM-9 and DOM-10.


Presentation: Sittampalam, Incremental execution of transformation specifications (Wed 2004-01-28, 12:30)

No abstract provided.


Presentation: de Moor, The miracle of C. and St Roland (Wed 2004-01-28, 15:00)

No abstract provided.


Presentation: Visser, Program transformation with scoped dynamic rewrite rules in Stratego (Wed 2004-01-28, 16:00)

Stratego/XT is a language and toolset for program transformation based on the paradigm of term rewriting with programmable rewriting strategies. In this talk I discuss the development in Stratego of a transformation component for constant propagation in an imperative language. The talk focuses on the dynamic generation of rewrite rules to propagate context-sensitive information.

The Stratego/XT system can be downloaded at www.stratego-language.org where one can also find a list of publications.

(The slides are available.)


Presentation: Goldberg, Certifiable stateflow compilation via partial evaluation (Thu 2004-01-29, 09:05)

No abstract provided.


Presentation: Backhouse, Algorithmic problem solving (Thu 2004-01-29, 10:00)

Algorithmic problem solving is a new introductory module on problem-solving, currently being given by the author at the University of Nottingham.

The goal of the module is to introduce the principles of designing algorithms that are correct by construction via well-known puzzles and games. This means that the problems posed are easily understood, and not ``mathematical'' problems in the sense of relying on previously known mathematical techniques (for their formulation and/or solution).

The three main programming principles we aim to introduce are invariants, problem decomposition and induction. Of these, the notion of an invariant is the most important, even though it is likely to be the most unfamiliar to the students. The module begins with simple examples that are easily solved using this concept. The other principles are introduced gradually, all three being integrated at later stages.

In this talk, I showed one of the highlights of the module, namely how to derive the specifcation of the mex function (used in determining a winning strategy in a two-person game) from its requirements. Briefly, a position in a ``sum game'' is the combination of a position in a ``left'' game and a position in a ``right'' game (which games may have different rules for moves). A move is a choice of a move in the left game or a move in the right game. A winning strategy is to introduce two functions on the positions in the component games, in such a way that the opponent can always be left in a position in which the functions have equal values. This is the requirement on the ``mex'' function, from which its formal specification can be derived.

Further information on the module can be obtained from my web page.

(The slides are available.)


Presentation: Cohen, The inner nexus (Thu 2004-01-29, 12:15)

No abstract provided.


Presentation: Hehner, Probabilistic predicative programming (update) (Thu 2004-01-29, 14:50)

No abstract provided, but see working paper.


Discussion: Dewar, Software patents (Thu 2004-01-29, 17:00)

No abstract provided.


Discussion: Boute, Mathematics in computer science education (Fri 2004-01-30, 11:40)

As a discussion topic, I would like to call the attention of the group to a serious problem that Computer Science curricula at certain universities are experiencing as a consequence of the recent Bachelor/Master reform. As a part of this reform, started in accordance with the Sorbonne/Bologna agreements, the universities in the European countries involved were required to design a 3-year Bachelor and a 2-year Master programme. In some places, the Bachelor programme is already implemented and conclusions can be drawn.

Some Bachelor programmes in Computer Science for engineering students contain no logic and no mathematics of programming. "No" is not a hyperbole but is to be taken literally. This omission of essential fundamental material is due to the pressure of including more material that is directly job-related as early as possible in the curriculum. Initially, there were promises to compensate for this deficiency in the Masters programmes, but recently approved proposals indicate that these promises will often not materialize. Arguments typically given are that "the mathematics of programming is for pure scientists, not engineers", and that "our engineering students find it too abstract and do not like it".

By talking this problem over with colleagues from many different countries, I found out that situations as described are not unique.

The relevance to WG2.1 is that university students graduating from such weakened curricula will be considerably less able to appreciate or even understand the kind of work this Working Group is doing than their predecessors. Since the health of any activity or branch of science heavily depends on a continuous influx of fresh, talented and well-prepared graduates, this is a serious reason for concern. It is therefore worthwhile for WG2.1 to discuss initiatives that might lead to improving the situation.

(A paper is available.)



Working documents

833 DOM-1
Graham Hutton. Compiling exceptions correctly (slides).

834 DOM-2
Graham Hutton and Joel Wright. Compiling exceptions correctly (draft paper).

835 DOM-3
Jeremy Gibbons. Streaming algorithms (slides).

836 DOM-4
Raymond Boute. Balancing the mathematical content of computing curricula.

837 DOM-5
Rick Hehner. Probabilistic Predicative Programming update.

838 DOM-6
J. Desharnais, B. Möller, G. Struth. Termination in Modal Kleene Algebra. Institut für Informatik, Universität Augsburg, Report 2004-04.

839 DOM-7
B. Möller, G. Struth. Greedy-Like Algorithms in Kleene Algebra. Institut für Informatik, Universität Augsburg, Report 2003-011.

840 DOM-8
T. Ehm, B. Möller, G. Struth. Kleene Modules. Institut für Informatik, Universität Augsburg, Report 2003-10.

841 DOM-9
B. Möller, G. Struth. Modal Kleene Algebra and Partial Correctness. Institut für Informatik, Universität Augsburg, Report 2003-08.

842 DOM-10
J. Desharnais, B. Möller, G. Struth. Kleene Algebra With Domain.

843 DOM-11
Eelco Visser. Program Transformation with Scoped Dynamic Rewrite Rules in Stratego (slides).

844 DOM-12
Clare Martin, Sharon Curtis, Ingrid Rewitzky. Modelling Nondeterminism.

845 DOM-13
Roland Backhouse. Algorithmic Problem Solving (slides).



Jeremy Gibbons (email: Jeremy.Gibbons@comlab.ox.ac.uk)