Contents of this page: Administrative matters | Technical presentations(Last updated 1st April 2004.)
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.
From Meeting 59, the secretary will send out formal invitations by email, emphasizing the points mentioned above.
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.
The group would like to express their thanks to Brian Wichmann for carrying out this noble task.
No abstract provided.
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.)
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.
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.)
No abstract provided.
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.)
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.
No abstract provided.
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.
No abstract provided.
No abstract provided.
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.)
No abstract provided.
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.)
No abstract provided.
No abstract provided, but see working paper.
No abstract provided.
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.)