Contents of this page: Local information | Proposed topics for discussion | Proposed talksMinutes of the meeting are now available (last updated 17th February 2004).
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.
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.Draft paper, and slides.
(Joint work with Joel Wright.)
Draft paper available. (Hasn't entirely decided yet whether to go.)
The abstract axiomatic semantics for weakest preconditions and strongest postconditions is often somewhat nonintuitive. Intuitive understanding can be greatly enhanced by calculationally deriving the "axioms" from simpler and more direct formulations of program behaviour, here called "program equations" by analogy with circuit equations. From Eric Hehner's presentation on probabilistic programming it is apparent that his formulation and program equations are very similar, and arguably represent the simplest possible way of expressing program behaviour.By formal calculation using a functional predicate calculus, weakest precondition and strongest postcondition semantics are derived as theorems. Right from the start, all calculations were guided by the "shape of the formulas", and went very smoothly where intuition was uncertain; afterwards one could "sit back and enjoy" the intuitive interpretation of the intermediate and final results. This is illustrated by the calculations for assignment, sequences, choice and iteration. The calculations show that the inadequacy of relations in properly handling nondeterminacy and termination (as Gordon pointed out in his notes "Specification and Verification I") is fully resolved in a simple and elegant way by introducing a separate termination predicate.
The subsection on loops, which was tentative at the time of the meeting, is completed in the updated version.
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.
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 comfluence and propositional Hoare logic.
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.