Background and outline of the Project


It is a central aim of Computer Science to provide techniques for developing software that is guaranteed to be correct and easy to maintain. The general objective of this project is to provide foundational contributions to this aim using domain- and proof-theoretic methods.

Domain theory and proof theory are branches of Mathematical Logic with important applications in Computer Science. In domain theory a great variety of data types and programming concepts can be modelled and analysed. This includes nondeterminism, computations on continuous and higher type data, and the operational semantics and expressive power of functional languages. On the other hand proof theory provides formal methods for program development. For example, the so-called `proofs-as-programs paradigm', according to which a constructive proof of a specification corresponds to a satisfying program, has led to a method of program synthesis from proofs which has been implemented in a number of interactive proof systems.

It is the objective of this project to pursue current research on the above mentioned applications of domain theory and proof theory in Computer Science, and to strengthen the existing links between these fields.

In domain theory various open problems in connection with the computational and topological structure of partial and total higher type functionals will be investigated. In particular, we will study and compare different models of computation (via approximation, numbering, functional programming, restricted forms of recursion), and investigate to which extent methods of studying computability on structures like metric, topological, or Banach spaces can be lifted to higher types, if possible retaining equivalence results as obtained in.

On the proof-theoretic side it is planned to further develop and improve the interactive proof system Minlog and its program extraction mechanism. Minlog's program extraction method is based on a variant of Kleene's realisability. This method, has a great potential of being extended and being made more flexible which apparently has not yet been fully exploited. In the project this potential shall be thoroughly investigated and implemented.

Domains are getting involved in program synthesis by extracting domain-theoretic algorithms (i.e. computable mappings between domains) from proofs, instead of concrete programs. This will give us the possibility to freely `invent' domain-theoretic realisers of critical axioms (e.g. nonconstructive choice principles) without being committed to a specific formal language. In this way, domain-theoretic insight in computational phenomena may be directly used for improvements and extensions of the formal proof calculus. In particular results on higher type functionals will be important, since such functionals almost inevitably occur in programs extracted from proofs.

The general idea of our domain-theoretic method of program synthesis is to separate logical from computational issues: The formal logical calculus is supposed to capture a mathematical subject and its proof methods at a high level of abstraction without being specific about computational details, whereas the computational model can be developed and studied informally using classical mathematical methods. Nevertheless, the logical and the computational world are firmly linked by the realisability interpretation. This means that classical mathematical concepts and proofs can be used more or less as they are, and need not be constructivised in order to get hold on their computational content.

We also would like to point out that the interaction of domain theory and proof theory via realisability suggested here is quite different from the use of realisability models as a general approach to domain theory. While we are studying specific topics (models of the reals etc., totality, higher types) in a relatively small part of domain theory (effective consistently complete algebraic (or continuous) dcpos) the latter provides a framework for the global theory.

Case studies exploring possible areas of application will play an important role in the project. Examples of program extraction in term rewriting and infinitary combinatorics will be studied. As a new and very promising enterprise we want to do `proof mining' (D.S. Scott) in computable and constructive analysis, building on our enhanced realisability interpretation and on domain-theoretic representations of the real numbers and related structures. We expect that our strategy of separating logical from computational issues will lead to more concise and transparent formalisations of analysis. Presently, constructive formalisations of analytical proofs often suffer from complicated representations of the reals and other basic analytical concepts reflecting a particular model of computation. The methods proposed in this project will make a formalisation of these models unnecessary, and thus will considerably facilitate program synthesis from analytical proofs.