Does a system actually do what it is supposed to do? Reasoning about huge systems is necessary and difficult. Our work pushes the limits of proof, builds tools using constructive type theory and logics, and applies them to problems such as railway signaling systems.

Higher order methods for semantics and program synthesis

Higher type semantic models and proof theory are important tools for analysing functional languages and automatically synthesising correct programs. Dr Ulrich Berger has developed a domain-theoretic notion of totality and used it to clarify the relationship between different models of computability in higher types. He is using this theory to develop a powerful technique for proving termination of functional programs.

On the proof theoretic side, Dr Monika Seisenberger and Dr Berger are collaborating with Professor H Schwichtenberg and his research group at the University of Munich to develop advanced methods of program synthesis from proofs, including constructive and non-constructive logics as well as logics for polynomial time computability. Many of the theoretical results have been implemented and have been applied in various fields, for example in infinitary combinatorics, computable analysis and higher order term rewriting. An example of a practically useful program extracted automatically from a formal proof is an efficient higher order term rewriting algorithm called normalisation by evaluation.

Proof theory, dependent type theory and applications

Hilbert’s Second Problem is to determine the limit of formal reasoning, and this has become one of the main aims of the theory of proofs. Dr Anton Setzer has determined the strength of various extensions (universes, W-type, reflection principles) of Martin-Löf type theory, including the Mahlo universe and the ∏3-reflecting universe, which are the strongest formal theories currently available in constructive logic.

A more practical goal is to apply the expressiveness of dependent types to programming technology, in the areas of generative and of provably correct programming. Together with Dr Peter Hancock (Edinburgh), Dr Setzer has introduced concepts for representing state-dependent interactive programs in dependent type theory, including a state-dependent monad. Dr Setzer, Fredrik Forsberg and Professor Peter Dybjer (Gothenburg) have developed the concept of inductive-recursive definitions and inductive-inductive definitions, which allows one to analyse and manipulate data structures — a very general form of generic programming. Dr Setzer has as well developed an integration of object technology into dependent type theory. Furthermore, he has with Karim Kanso fully verified real world railway interlocking systems in such a way that the code to be executed is identical to the code to be verified, avoiding errors in the translation.