Proof and Counterexample

Greg Restall is
writing a book, entitled Proof and Counterexample (or PnC for short). It's on logic viewed through the lens of proof theory. In particular, it covers natural deduction, sequent calculus, normalisation and cut-elimination. It's designed to both be state-of-the-art reseearch on these topics, together with an introduction appropriate for an advanced undergraduate. (We'll see how that works. I'll be test-driving the material with honours students from February to June in 2005.)

These pages will contain all sorts of different material about the book: comments, discussion, pointers to related material, and anything else that the community behind this site sees fit to write.

Newcomers to the field might wonder why this is relevant to programming languages, and some readers would regard this as pointless theory...

But if you are one of us guys excited by Curry-Howard, you might enjoy this wiki a lot.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

A gift for understatement

But if you are one of us guys excited by Curry-Howard, you might enjoy this wiki a lot.

You might be right!

Natural language...

You will surely enjoy it. You might enjoy it a lot...

Cool typesetting

At the moment, I am mostly enjoying his typesetting.


Thanks for the kind words. It's very early days yet, but the place (and the draft) will develop a lot in the next few months, as I teach the material with honours students.

I'll also be teaching from it at the ASL Summer Colloquium in Athens in July/August, and at then at ESSLLI 2005, so any feedback/comments/hints/help/etc., are most appreciated.


Hi Greg,

Is there any chance you will be in Lisbon for our Structures and Deductions workshop? We're hoping that, from your neck of the woods, Rajeev Gore will make it.


Wish I was able to come. It's at the start of my study leave for 2005 (from July), but I'm committed to be in Denmark looking after my son while my spouse is working on a research project there for a couple of weeks. I'm back doing work at ASL05 in Athens, and then ESSLLI2005 (and then I'll be based in Oxford after that for a bit). I'm hoping to get to the continent again some time between September and December.

Child care

I'll email Greg privately, but in case any one else is interested in attending SD05, but thinks they can't because of childcare responsibilities, we will be organising proper childcare facilities, since quite a few attendees will be in the same boat.

thought you said

Curly Howard in which case I'd have to agree too. :-)