projects
International Research Cooperations
The Laboratory for Mathematical Logic and Theoretical Computer Science is partaking in several international research cooperations:
 EUProjekt CORCON (20142017)
 EUProjekt COMPUTAL (2012–2015)
 GermanyChina (2008–2011)
 GermanyRussia (2005–2011)
 GermanySouth Africa (2007–2011)
EUProjekt CORCON (20142017)
Topic:
Correctness by Construction
Funding:
EUFP7Programme IRSES
Coordinator:
Dr. Peter Schuster (Leeds)
Participating groups and institutions:
 Australia:

 Dr. Pattinson (Canberra, ANU)
 Germany:

 Prof. Dr. Schwichtenberg (Munich, LMU)
 Dr. Diener, Prof. Dr. Spreen (Siegen)
 United Kingdom:

 Dr. Schuster, Dr. Beyersdorff, Prof. Rathjen, Dr. Stell (Leeds)
 Prof. Gani (Glasgow, U Strathclyde)
 Drs. Berger, Blanck, Seisenberger, Setzer (Swansea)
 India:

 Prof. Mahajan (Chennai, Inst. Mathematical Sci.)
 Italy:

 Dr. Benini (Varese, U della Insubria)
 Profs. Moggi, Rosolini (Genua)
 Prof. Sambin (Padua)
 Japan:

 Prof. Ishihara (Nomi, Ishikawa, Japan Inst. Science and Technology)
 South Korea:

 Prof. Lee (Anseongsi, Hankyong Nat. U)
 New Zealand:

 Prof. Bridges (Christchurch, U Canterbury)
 Sweden:

 Profs. MartinLöf, Palmgren (Stockholm)
 USA:

 Profs. Awodey, Avigad, Harper, Sieg (Pittsburgh, CMU)
 Associated partners:

 Dr. Benini (Varese, U della Insubria)
 Profs. Tsuiki, Sato (Kyoto)
 Prof. Tatsuta (Tokyo, Nat. Inst. Informatics)
 Prof. Tanaka (Sendai, Tohoku U)
 Profs. Coquand, Dybjer (U Gotheburg)
 Prof. Bauer (Ljubljana)
Project summary:
As software becomes ever more ubiquitous in our lives, the need to ensure it runs without error becomes ever more important. Restarting a phone is a simple, if inconvenient task; restarting an aeroplane in midflight is not an option! Correct by construction programming offers a revolutionary approach to program verification where programs can contain not just computations as is normal, but also logical proofs of the correctness of these computations. The simple fact that such programs compile provides formal, i.e. mathematical, guarantees of the correctness of the program. In particular, there is no need for posthoc testing of software etc. Fundamental to the implicit marriage of computation and logic inherent within correct by construction programming is the choice of the right logical systems and concepts upon which programming languages ought to be built. This reflects the symbiotic relationship between logic, programming, and the design of programming languages—any attempt to sever this connection will diminish each component. This proposal brings together internationally leading researchers from both inside Europe and outside Europe to work on exactly what logical structures are needed for correct by construction programming and how those logical structures can then by turned into concrete programming artefacts. In order to produce fundamental work which stands the test of time, we work not with specific programming languages but with mathematical abstractions of them. The recent development of dependently typed programming languages capable of supporting correct by construction programming makes this a very timely proposal, while the billions spent on software every year makes the potential impact of this proposal very significant.
EUProjekt COMPUTAL (2012–2015)
Topic:
Computable Analysis
Funding:
EUFP7Programmschema IRSES
Coordinator:
Prof. Dr. Dieter Spreen (Siegen)
Participating groups and institutions:
 Germany:

 Prof. Dr. Peter Hertling (Uni Federal Forces Munich)
 Prof. Dr. Dieter Spreen (Siegen)
 Prof. Dr. Norbert Müller (Trier)
 Prof. Dr. Martin Ziegler (Darmstadt)
 UK:

 Dr. Ulrich Berger (Swansea)
 Prof. Anuj Dawar (Cambridge)
 Japan:

 Prof. Hajime Ishihara (Japan Advanced Institute ofScience and Technology, Nomi, Ishikawa)
 Russia:

 Prof. Victor Selivanov (A.P. Ershov Instituteof Informatics Systems, SBRAS, Novosibirsk)
 Slovenia:

 Prof. Dr. Andrej Bauer (Ljubljana)
 South Africa:

 Prof. Vasco Brattka (University of CapeTown)
 Prof. HansPeter Künzi (University of CapeTown
 Prof. Willem Fouché (University of SouthAfrica, Pretoria)
 Associated partners:

 Prof. Hideki Tsuiki (Kyoto University)
 Prof. Dr. Klaus Weihrauch (Fernuniversität Hagen)
 PD. Dr. Robert Rettinger (Fernuniversität Hagen)
Project summary:
The programme of this interaction focusses 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 safetycritical 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 welldeveloped analytical theories based on the nonconstructive concept of a real number. Implementations, on the other hand, use floatingpoint realisations of real numbers, which do not have a wellstudied 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.
GermanyChina (2008–2011)
 Topic:
 Computability andComplexity in Analysis: Towards a Sound Foundationfor Scientific Computations
 Funding:
 German Science Association(DFG) – Natural Science Foundation of China
 Coordinators:

Prof. Dr. Dieter Spreen(Germany) Prof. Dr. Decheng Ding(China)  Participants:

 On the German side thefollowing groups are
participating:
Prof. Dr. Klaus AmbosSpies(Heidelberg) Prof. Dr. Peter Hertling (Uni FederalForces Munich) Prof. Dr. Klaus Meer (Cottbus) Prof. Dr. Norbert Müller (Trier) Prof. Dr. Dieter Spreen (Siegen) Prof. Dr. Klaus Weihrauch (Hagen) Prof. Dr. Martin Ziegler (Darmstadt).  The Chineseparticipants are:
Prof. Dr. Decheng Ding (NanjingUniversity) Prof. Dr. Dianchen Lu (Jiangsu University, Zhenjiang) Prof. Dr. Hong Lu(Nanjing University) Prof. Dr. Kaile Su (BeijingUniversity) Prof. Dr. Wei Wang (Sun Yatsen University, Guangzhou) Prof. Dr. Yongcheng Wu (Nanjing University of Information Science andTechnology) Prof. Dr. Daoyun Xu (Guizhou University,Guiyang) Prof. Dr. LiangYu (Nanjing University) Prof. Dr. XishunZhao (Sun Yatsen University, Guangzhou) Dr. Qingliang Chen (Jinan University, Guangzhou) Dr. Xuxin Mao (Nanjing University ofAeronautics and Astronautics) Dr. Yun Fan(Southeast University, Nanjing).
 On the German side thefollowing groups are
participating:
 Project summary:

In safetycritical 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. An
important example are autopilot systems for aircrafts.
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 welldeveloped analytical theories based on the nonconstructive concept of a real number. Implementations, on the other hand, use floatingpoint realizations of real numbers which do not have a wellstudied mathematical structure. Ways to get out of these problems are currently promoted under the slogan “Computing with Exact Real Numbers”. They are based on the following ideas:
In traditional analytical mathematics, points of spaces represent the “ideal (total)” result of approximations. In order to give a sound mathematical semantics to programs that have data structures representing such points, the “partial (finite)” objects used to approximate them have to be given the same status of points of a space as the total ones. From a computational view point they are even the firstclass citizens, as the other—the total—ones are derived via a limiting process. This has led to new structures (e.g. “domains” in the sense of Yu.L. Ershov and D.S. Scott).
For proving the existence of certain objects, for example the roots of polynomials or fixed points of operators, one can proceed in a purely abstract way using e.g. proofs by contradiction or compactness arguments. In applications, however, we need not only know that such objects exist, we need a concrete way to get hold of them. This can be achieved in a logicoriented way by either using a constructive framework in the existence proof or by disclosing the constructive content of classical proofs, or by deriving an effective version of the classical existence result, i.e. by studying whether and how the postulated object can be computed. The latter approach—to a large extent developed by K. Weihrauch and his students and known as TypeTwo Theory of Effectivity (TTE)—has led to extensions of traditional models used for computations on discrete objects and the study of their complexity. The full relationship of these approaches is still under investigation.
A typical feature of computability and of the algorithms doing the computation is their deterministic rulebounded behaviour. Opposed to this, in the physical world we often have to deal with processes the outcomes of which exhibit a “lawless” (random) behaviour. Considerable effort has been put in making this notion precise, leading among others to the development of the theory of algorithmic randomness and of algorithmic information theory. This allows new insights in such fundamental phenomena as noncomputability.
The research in this project concentrates on the following interrelated problem areas:
 Computability notions and models for real numbers.
 Effective versus constructive topology.
 Algorithmic randomness.
 Computability and complexity in higherorder and abstract spaces.
 Datastructures and efficient algorithms.
The project is a followup of a similar earlier one.
GermanyRussia (2005–2011)
 Topic:
 Computations overnondiscrete structures: models, semantics and complexity
 Funding:
 German Science Association(DFG) – Russian Foundation for Basic Research
 Coordinators:

Prof. Dr. Dieter Spreen(Germany) Prof. Dr. Yuri L. Ershov (Russia)  Participants:

 On the German side the following groups are
participating:
Prof. Dr. PeterHertling (Uni FederalForces Munich) Prof. Dr. Klaus Keimel (Darmstadt) Prof. Dr. UlrichKohlenbach (Darmstadt) Prof. Dr. Christian Herrmann (Darmstadt) Prof. Dr. Helmut Schwichtenberg (LMUMunich) Prof. Dr. Dieter Spreen (Siegen) Prof. Dr. Thomas Streicher (Darmstadt) Prof. Dr. Klaus Weihrauch (Hagen) Prof. Dr. Martin Ziegler (Darmstadt).  The Russianparticipants are:
Prof. Dr. YuriL. Ershov(Novosibirsk) Prof. Dr. Sergei S. Goncharov (Novosibirsk) Prof. Dr. Andrei S. Morozov (Novosibirsk) Prof. Dr. Victor L. Selivanov(Novosibirsk) Dr. Vladimir Bashkin (Novosibirsk) Dr. Margarita V. Korovina (Novosibirsk) Dr. Alexandre Kravchenko(Novosibirsk) Dr. OlegV. Kudinov (Novosibirsk) Dr. Vadim G. Puzarenko (Novosibirsk) Dr. Marina V. Semenova (Novosibirsk) Dr. Alexei Stukachev (Novosibirsk).
 On the German side the following groups are
participating:
 Project summary:

It appears that the intuitive notion of computability
in our everyday life actually exists for a broader
class of basic structures, not only for the natural
numbers or other discrete structures such as the
rational numbers, lists, finite strings, etc. The most
important structure not in this list is the set of real
numbers. Computations involving real numbers abound in
engineering and the applied sciences. In these
applications real numbers are identified with sequences
of rational approximations (which serve as a name for
the real number). The computations are done on finite
parts of such approximations and produce approximations
of the result. In other words, the computations are not
performed on the real numbers, which are abstract
mathematical entities, but on concrete objects
representing them. Such concrete objects can in general
be coded by sequences of natural numbers or finite
words, i.e., one computes on Baire and/or Cantor space.
In safetysensitive areas such as aircraft control it is important that correctness of the used software is formally verified. Starting from a given program this is mostly a hard task. An appealing idea is therefore to try to extract the algorithm that has to be developed from a formal proof of its specification. This idea has first been introduced for formal systems of constructive logic, but proofs in analysis usually use clas sical logic. Moreover, it has turned out that even in the case of constructive logic, the complexity of the extracted algorithm might be unfeasible.
Feasibility is an important issue, not only for algorithms on the reals. In many applications such algorithms are known if one allows algorithms that have nondeterministic or probabilistic features. Other applications require the combination of discrete and continuous computations. Appropriate programming languages have to be designed for these tasks, the semantics of which must be defined in a precise way. New mathematical tools are needed to this end.
Systems that combine discrete and continuous computations (hybrid systems) are broadly used nowadays, e.g., in electromechanical systems (robots), in air traffic control, in the control of automated free ways, and in chemical process control. In many cases the discrete part of such a system uses a simple and highly effective model of computation, which is no longer Turingcomplete, e.g. finite automata. Although finite automata fail to serve to solve all decidable problems, they are powerful enough in many situations and algorithms based on them are very fast. Moreover, most of the important problems for them are algorithmically decidable. Parallelism is an important feature of the algorithms used in this area. So Petri nets and similar concepts come into play very naturally.
The research in this project concentrates on the following interrelated problem areas:
 Computability and complexity overtopological structures.
 Topological models of higher typecomputations.
 Approximable functionals in typetheory.
 Proofmining in analysis.
 Complexity in incomplete models ofcomputability.
The Project is a followup of two similar ones.
GermanySouth Africa (2007–2011)
 Topic:
 From continuity tocomputability
 Finanzierung:
 DeutscheForschungsgemeinschaft – National ResearchFoundation of South Africa
 Coordinators:

Prof. Dr. Dieter Spreen(Germany) Prof. Dr. Vasco Brattka(South Africa)  Participants:

 On the German side thefollowing groups are
participating:
Prof. Dr. PeterHertling (Uni FederalForces Munich) Prof. Dr. KlausKeimel (Darmstadt) Prof. Dr. UlrichKohlenbach (Darmstadt) Prof. Dr. NorbertTh. Müller(Trier) Prof. Dr. HelmutSchwichtenberg (LMUMunich) Prof. Dr. DieterSpreen (Siegen) Prof. Dr. ThomasStreicher (Darmstadt) Prof. Dr. KlausWeihrauch (Hagen) Prof. Dr. MartinZiegler (Darmstadt).  The South Africanparticipants are:
Prof. Dr. VascoBrattka (University of CapeTown) Prof. Dr. Willem Fouché (University of SouthAfrica, Pretoria) Prof. Dr. HansPeter Künzi (University of CapeTown) Prof. Dr. Petrus H. Potgieter(University of SouthAfrica, Pretoria) Dr. George Davie (University of SouthAfrica, Pretoria) Dr. Paul Potgieter (University ofSouth Africa,Pretoria).
 On the German side thefollowing groups are
participating:
 Project summary:

It appears that our intuitive notion of computability
makes sense not only for discrete structures as natural
numbers, rational numbers, lists, finite strings etc.,
but for a much broader class of nondiscrete structures
like real numbers and other spaces. Computations with
real numbers abound in engineering and in the applied
sciences. In these applications, real numbers are
identified with sequences of rational approximations
and computations are executed on finite parts of such
approximations and produce approximations of the
result.
In traditional topology, points of spaces represent the “ideal (total)” results of approximations. For the verification of procedures that compute such objects, the “partial (finite)” objects used to approximate them have to be given the same status of points of a space as the total ones. This has led to new structures (e.g. “domains” in the sense of Yu.L. Ershov and D.S. Scott) and a new branch of topology: “asymmetric topology”.
For proving the existence of certain objects, for example roots of polynomials or fixed points of operators, one can proceed in a purely abstract way using e.g. proofs by contradiction or compactness arguments. In applications, however, we not only need to know that such objects exist, we need a concrete way to get hold of them. This can be achieved in a logicoriented way by either using a constructive framework in the existence proofs or by disclosing the constructive content of classical proofs, or by deriving an effective version of the classical existence result, i.e., by studying whether and how the postulated object can be computed (computable analysis). Obviously, these approaches are closely related.
A typical feature of computability and of the algorithms doing the computation is their deterministic rulebounded behaviour. Opposed to this, in the physical world we often have to deal with random processes. Considerable effort has been put in the development of a notion of algorithmic randomness and of algorithmic information theory. This allows new insights in such fundamental phenomena as noncomputability.
The research in this project concentrates on the following interrelated problem areas:
 Computability over topological structures:computable analysis and topology.
 Constructive ways to topology andmathematics.
 Topological models of computability:domains and asymmetric spaces.
 Approximable functionals in typetheory.
 Proofmining in analysis, hyperbolic geometry andgeometric group theory: obtaining uniformeffective bounds.
 Kolmogorov complexity, Brownian motion,randomness, dynamical systems.