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

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.