This week in Categorical Logic: a Baez celebration of sorts...

So I never get sick, mostly, but when do, I'm a total wimp. I feel like it's bad, horrible, terrible and that things will never be the same again. Pathetic, I know.  But since I got the unexpected gift of being sick for the last two days I was able to notice this proposed celebration of John Baez "This week in mathematical physics" 20-year anniversary. Cool, isn't it? So I thought I'd have a go.

I'm not a conventional mathematician and not a math blogger really, but I do blog occasionally about maths an other scientific pursuits, so why not?

I also gives me an excuse to enjoy a two hour leisurely tour of what I think it's fun, nice and new in categorical logic. Like the proposer of the celebration says I will try to describe with capsule summaries  ``a few papers I’ve recently noted with pleasure and interest", but I am very much behind of my reading on anything mathematical, so it won't be this week's finds at all. I also decided to give myself a maximum of 5 papers/programmes to describe so that the task doesn't look to big and I fail to even start it. I can always add some people/ideas later on if I want to.

1. The Univalent Foundations, Voevosky et al has to be the first big new thing in categorical logic in the last few years. I don't pretend to understand any of it, but it sure is about the equality of proofs in type theory, which is categorical logic par excellence. Apart from the IAS link above one can read about it from Thierry Coquand, Steve Awodey, Peter Lumsdaine and many other excellent category theorists. I thought I was going to do a "for-dummies" version, but haven't had the time, yet.

2. Olivia Caramello's programme of Topos Theory as a unifying force in mathematics. I don't know much about this either, I haven't even read the "for-dummies" versions that she presents in her site, so I'm looking forward to another sudden sickness to catch up on this...

3. The computational content extraction from (classical) proofs is still going strong and while it's mostly done without categorical logic (Kohlenbach's website contains many excellent examples of what has been re-branded as "proof mining" e.g. Gödel's functional interpretation and its use in current mathematics.), the hope has always been that categorical logic will play a bigger part. I was/am particularly excited by Paulo Oliva's work, but then I'm biased as his work is/was remotely related to mine. (There are lots of new publications in Paulo's webpage, need to check them out.)

4. It is only fitting that one of my interesting programmes in categorical logic has to do with John Baez and particularly Mike Stay with whom I've discussed some of these issues. I'm referring to their manifesto Physics, Topology, Logic and Computation: A Rosetta Stone . (I'm afraid I haven't read it, just skimmed it enough to know I should!) I once gave a talk to the physicists in Cambridge's DAMPT (invited by my friend Shaun Majid) which was enough to convince me that there's plenty of easy stuff to do in the frontiers between categorical logic and several kinds of theoretical physics that would be very useful to both communities.

5. Finally I want to end up with something that it's not like a programme yet, but I hope it will become one, given the right conditions... This paper is an intriguing connection between logic, distributed programming in the large and Milner-style tacticals (as in LCF, HOL, Isabelle, etc...).
I don't the differences between that  and this, so adding both links here.

As it probably isn't clear from the short descriptions above, my own work is related to 3, 4 and 5 above.  And I will not be surprised if the Dialectica and its models are also connected to 1 and 2... 
Had I not had to earn a (very comfortable) living I guess I would be working on the programmes above. Since I do have to earn one, I'm instead working on the also very exciting themes of Logic for and from Language. I guess it would also be fun to list the best big ideas (as far as I'm concerned) on that front too. After all this is about the only good thing about getting old: you get much more convinced of your ideas and that they're worth spreading...

(picture by Eric Volpe, check his flickr stream)