In safety-critical applications it is not sufficient to produce software that is only tested for correctness: its correctness has to be formally proven. This is true as well in the area of scientific computation. The problem here is that the current mainstream approach to numerical computing uses programming languages that do not possess a sound mathematical semantics. Hence, there is no way to provide formal correctness proofs.

The reason is that on the theoretical side one deals with well-developed analytical theories based on the non-constructive concept of a real number. Implementations, on the other hand, use floating-point realizations of real numbers which do not have a well-studied mathematical structure. Ways to get out of these problems are currently promoted under the slogan "Computing with Exact Real Numbers".

Well developed practical and theoretical bases for exact real number computation and, more generally, computable analysis are provided by Scott's Domain Theory and Weihrauch's Type Two Theory of Effectivity (TTE). In both theories real numbers and similar ideal objects are represented by infinite streams of finite objects.

The seminar focused on two problem areas in the realm of computable analysis and computation on infinite streams:

1. Algorithms for stream transforming functions with particular emphasis on (i) logical and category-theoretic methods for the synthesis of provably correct programs, (ii) topological investigations of particular stream representations supporting efficient stream algorithms.
2. Hierarchies and reducibility relations between sets and functions of infinite data as a means of classification. Methods from topology, logic and descriptive set theory were of particular importance in this case.

Infinite streams are infinite words, So there is a close connection to the theory of omega-languages. To study these was a further aim of the seminar. In the last years much interest in the (logical and topological) structure of the infinite words used to represent continuous data as well as how they code the data space has emerged. U. Berger and others are developing a constructive theory of digital computation based on co-induction, and are applying it to computable analysis. The aim is to create a mathematical foundation for (lazy) algorithms on analytical data such as real numbers, real functions, compact sets, etc. Since co-induction admits a particularly elegant formalization, this approach is well suited for computer aided modeling and proving in computable analysis. A concrete goal is to use program extraction from proofs as a practical method for obtaining certified programs in computable analysis.

The theory is based on a category of digit spaces. A typical object in this category is a compact metric space with a set of digits, where each digit is a contracting map. A point is then an infinite sequence of function (digit) compositions and hence represented by the corresponding infinite word. Moreover, for any given finite length, the words of that length over the alphabet of digits define a covering of the given space that allows to exactly locate the points represented by infinite words of digits. The set of uniformly continuous functions between such spaces can be characterized by a combined inductive/co-inductive definition that gives rise, via program extraction, to implementations of such functions as non-wellfounded (lazy) trees. The theory of digit spaces combines known techniques for implementing and verifying stream processing functions (Edalat, Pattinson, Potts, and others) with ideas from co-induction and co-algebra (Jacobs, Rutten, Bertot, Niqui, and others).

H. Tsuiki is pursuing a similar programme, though, from a different perspective. In his case, e.g., every infinite object is represented by exactly one infinite word over { 0, 1, \bot \}, where bot represents "unknown''. It turned out that the encoded space has at most topological dimension n, exactly if there are not more than $n$ occurrences of bot in the corresponding infinite code words. Besides the problem of how to represent continuous data in an ``optimal'' way, it is as well an important task to distinguish between computable and non-computable functions and, in the last case, to estimate the degree of non-computability. Most functions are non-computable since they are not even continuous. A somewhat easier and more principal task is in fact to understand the degree of discontinuity of functions. This is mostly achieved by defining appropriate hierarchies and reducibility relations.

In classical descriptive set theory, along with the well-known hierarchies, Wadge introduced and studied an important reducibility relation on Baire space. As shown by van Engelen et al., von Stein, Weihrauch and Hertling, this reducibility of subsets of topological spaces can be generalized in various ways to a reducibility of functions on a topological space. In this way, the degrees of discontinuity of several important computational problems were classified. It turned out that these classifications refine the so called "topological complexity'' introduced in the alternative Blum-Shub-Smale approach to computability on the reals, which is used in complexity considerations in computational geometry.

Recently, reducibilities for functions on topological spaces have been used to identify computational relations between mathematical theorems. This programme, started by V. Brattka et al., can be considered as an alternative to reverse mathematics. Whereas reverse mathematics focuses on set existence axioms required to prove certain theorems, the approach pursued in computable analysis is to identify the computational power required to ``compute'' certain theorems. The approach, with contributions by M. de Brecht, G. Gherardi, A. Marcone, A. Pauly, M. Ziegler and V. Brattka, has led to deep new insights into computable analysis and has revealed close relations to reverse mathematics, but also some crucial differences. Motivated initially by decidability problems for monadic second-order logic and Church's synthesis problem for switching circuits, researchers from automata theory (Büchi, Trakhtenbrot, Rabin, Wagner and many others) developed the theory of omega-languages which provides a foundation of specification, verification and synthesis of computing systems. Topological investigations in this theory have led to several hierarchies and reducibilities of languages of infinite words and trees. Instead of being just continuous, the reduction functions are now required to be computable by automata of suitable type. The resulting hierarchies (like, for example, the Wagner hierarchy) have sometimes the advantage that their levels are decidable.

Note that even the study of automata on finite words now involves topological methods in the classical form of profinite topology. Recently, deep relations of profinite topology to Stone and Priestly spaces were discovered by Pippenger and developed by Gehrke, Grigorieff and Pin. Again, suitable versions of the Wadge reducibility seem to play an important role in development of this field.

The seminar attracted 51 participants representing 15 countries and 5 continents, and working in fields such as computable analysis, descriptive set theory, exact real number computation, formal language theory, logic and topology, among them 10 young researchers working on their PhD or having just finished it. The atmosphere was very friendly, but discussions were most lively. During the breaks and until late into night, participants gathered in small groups for continuing discussions, communicating new results and exchanging ideas. The seminar led to new research contacts and collaborations. The participants are invited to submit a full paper for a special issue of Mathematical Structures in Computer Science. At least one submission deals with a problem posted in the discussions following a talk. The great success of the seminar is not only due to the participants, but also to the staff, both in Saarbrücken and Dagstuhl, who always do a great job in making everything run efficient and smoothly. Our thanks extend to both groups!