Alex Summers

Congratulations to Alex Summers whose PhD I examined with Hugo Herbelin at Imperial yesterday. Hugo and I (well, okay, mainly me) had lots of questions for Alex but he did a great job in answering them. His thesis addresses the question "what is the computational content of classical logic?" He looks at both sequent calculus and natural deduction formulations.

He has two very striking results. The first considers the question of adding ML-style polymorphism to classical logic. There are some old results from Harper et al. showing that this is non-trivial (i.e. unsound) but Alex shows that a proof theoretic approach can lead to sound answer. This is a very interesting result (we probably discussed this one result for an hour in the viva!).

The second striking result concerns his variant of the lambda-mu calculus. He derives a set of reduction rules that are able to simulate control operators with prompts. Until I read this I wouldn't have thought it possible. His calculus - the nu-lambda-mu calculus - is very elegant, and tidies up some of the loose ends that I tried to hide under the carpet when I was devising an operational theory for languages with control operators back in the nineties! If I had more time I'd probably go back to my old MFCS paper and see if the results would be improved by using a better calculus.

Anyway, Alex has some small changes to make but I'd expect his final version to be available soon. I recommend it to you!