Theory: Algebraic and Logical Design Methods
Proofs
- Higher order methods for semantics and program synthesis
- Proof theory
- Bounded arithmetic
- Type theory
The analysis and manipulation of formal proofs plays a central role in Logic and Computer Science and is a major field of research in the Logic and Computation group at Swansea. Our work covers reductive proof theory — exploring the limits of provability — constructive Type Theory and interactive theorem proving — providing new paradigms for program verification and program development — as well as proof-theoretic approaches to the grand challenges in computational complexity theory.
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. U Berger has developed a domain-theoretic theory of totality and used it to clarify the relationship between different models of computability in higher types. Currently he uses this theory to develop a powerful technique for proving termination of functional programs. On the proof theoretic side M Seisenberger and U Berger are collaborating with H Schwichtenberg and his research group at the University of Munich (LMU) in the development of advanced methods of program synthesis from proofs which include constructive and nonconstructive logics as well as logics for polynomial time computability. Many of the theoretical results have been implemented in the interactive theorem prover MINLOG and are 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
One of the main aims in proof theory is to determine the limit of formal reasoning (Hilbert's Second Problem). A 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 P3-reflecting universe, the strongest formal theories currently available in constructive logic. The more practical goal is to apply the expressiveness of dependent types to programming technology, in the areas of generative and of provably correct programming.
Bounded arithmetic
One of the most challenging problems in theoretical computer science and mathematics is the understanding of the relationship between complexity classes, most notably the P vs NP problem, which has been identified as one of the Millennium Problems by the Clay Mathematics Institute. Bounded arithmetic is an approach to analyse complexity-theoretic questions in the framework of mathematical logic, more precisely, in logical theories of arithmetic where quantification and induction are restricted ("bounded") in such a manner that complexity-theoretic classes can be closely tied to provability in these theories of bounded arithmetic. Beautiful connections of bounded arithmetic with complexity classes around the polynomial time hierarchy have been established in the mid 1980's by S Buss (UCSD). Since then, research in this area increases our understanding of the relationship between bounded arithmetic theories and its connections to other areas of complexity theory, in particular to proof complexity.
The major open problem for bounded arithmetic still is the question whether the hierarchy of bounded arithmetic theories collapses or not. This question is believed to be equally hard (even equivalent by some) to the question whether the polynomial time hierarchy collapses or not. Bounded arithmetic is one of the main topics in A Beckmann's research. In particular, A Beckmann is an expert in all kinds of proof theoretic investigations related to bounded arithmetic. A Beckmann invented "Dynamic Ordinal Analysis" which builds a bridge between classical branches in proof theory determining proof theoretic ordinals for all kinds of (mostly strong) mathematical theories and bounded arithmetic [paper]. Dynamic ordinal analysis characterises the proof and computation strength of bounded arithmetic theories, which is one of the topics in A Beckmann's EPSRC funded research project Abstract Measures of Low-Level Computational Complexity. A Beckmann has collaborated with S Buss (UCSD) and C Pollett (SJSU) on investigations of well orderings within bounded arithmetic [paper], and with J Johannsen (LMU) on the relation between linear bounded arithmetic theories [paper].
Type theory
Type theory was invented by Bertrand Russell at the beginning of the logical Renaissance at the beginning of the last century. There are two main research directions in type theory: non-dependent type theory, in which the set of types can be defined separately without knowing its elements, and dependent type theory, in which types can depend on elements of other types, and in which therefore types and the elements of the types have to be defined simultaneously. In Swansea research is carried out both in non-dependent and in dependent type theory.
Research on non-dependent type theory is mainly carried out by U Berger and M Seisenberger. Their specialities are domain theoretic models of type theory, totality in type theory, constructive inductive definitions and the extraction of programs from constructive and classical proofs. They use heavily the theorem prover Minlog both in research and teaching.
Research on dependent type theory is carried out by A Setzer. His speciality is Martin-Löf type theory (MLTT). MLTT is one of the most deeply researched areas of type theory, which is used as a foundation of constructive mathematics and as theoretical basis for more generic programming languages and for theorem provers. He carries out proof theoretic investigations in type theory and has developed the largest predicatively justified extensions of MLTT, namely the Mahlo universe and the Pi3-reflecting universe. In this context he has developed with Peter Dybjer a closed formalisation of inductive-recursive definitions, which is a very generic formulation of extensions of MLTT, which has applications in generic programming. He is as well investigating MLTT as a programming language, and has developed the notion of interactive programs, final coalgebras, and concepts of object-oriented programming in this type theory.
M Roggenbach is working on the connections between algebraic specifications and type theory. He has a strong background in the Common Framework Initiative, which recently finished the design of the algebraic specification language Casl. Together with the other members of his group, Y Isobe and A Gimblett, he develops, on the basis of the Munich theorem prover Isabelle, proof support for the process algebra Csp and the newly designed specification language Csp-Casl.
