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
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
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
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
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
(i.e. computable mappings between domains) from proofs,
instead of concrete
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
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
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
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
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.