research
# Research Interests -
Mathematical Logic and Combinatorics

My main interests are:

- frameworks for constructivism (constructive set theory, explicit
mathematics, Martin-Löf type theory);
- proof theory (principally ordinal analyses of theories);
- set theory (chiefly admissible set theory and large "cardinals" in
constructive set theory);
- combinatorial principles (Kruskal's theorem,...).

### Proof Theory

Proof theory includes the following topics:
infinitary proof theory and ordinal analysis, proof transformations and
program synthesis, and connections with subrecursive complexity.
There is a fundamental question which, since the pioneering
contributions of Gödel, Gentzen and Herbrand over fifty years ago, has
motivated the continued development of that area of Mathematical Logic
known as "Proof Theory", and which now drives much present-day activity in
Theoretical Computer Science, namely "What is the information content of a
constructive formal proof and how can it be read off ?" or, more
specifically, "How is it possible to synthesize programs from formal
proofs of their specifications , and hence classify and compare them - and
the functions which they compute - according to their proof -theoretic
complexity ?"

If, from a formal proof of the specification, it were possible
effectively to extract or synthesize a program P which satisfies it, then
the program would automatically be a "verified" one. If, in addition, it
were possible to read off from the proof, bounds on the existential
theorems occurring in it, this would provide an effective way of
estimating the complexity of P. If this connection between proofs and
programs were sufficiently close, then "natural" transformations on proofs
would correspond to natural program transformations. Mathematical logic
provides theoretical realizations of these possibilities, based on the
deep and well known correspondence which exists between proof-rules and
recursive program-constructs.