The conference of the same name

Interactive Theorem-Proving is not just the name of this web-log, but is also the name of a conference due to happen in 2010 as part of the Federated Logic Conference (FLoC) in Edinburgh. ITP will also continue as a separate conference subsequently.

Ex nihilo

I’ve created this blog so as to give myself an OpenID. But I suppose it’s just possible I’ll become seduced by the whole interface and use it for more than just that.