The programme of this interaction will focus on the following related topics: computable analysis, domain theory, topology, and exact real number computation, hereby dealing with both theoretical and applied aspects. A major motivation for undertaking this research is the fact that 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 also true in Scientific Computing. 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 certain applications also other computational models are used. Moreover, strengthening the underlying logic has been suggested. The full relationship of these approaches is still under investigation. Weihrauch's TTE is based on Turing machines that by computing infinitely long transform infinite strings. The study of such computations is important also for other branches of theoretical computer science including specification, verification and synthesis of reactive systems as well as stream computability. In contrast to the theory of finite computations, the study of infinite computations crucially depends on topological considerations.    «

The programme of this interaction will focus on the following related topics: computable analysis, domain theory, topology, and exact real number computation, hereby dealing with both theoretical and applied aspects. A major motivation for undertaking this research is the fact that 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 also true in Scientific Computing. The problem here is t...    »