### Semantics of Proofs in Paris

#### Posted by John Baez

There’s going to be a “thematic trimester” in Paris starting next spring:

- Semantics of proofs and certified mathematics, Institut Henri Poincaré, April 22nd - July 11th, 2014, organized by Pierre-Louis Curien, Hugo Herbelin, Paul-André Melliès.

If you like applications of category theory to logic and computer science, there should be a lot for you here!

The basic layout is this:

- Week 1 — Kick-off: Formalisation in mathematics and in computer science
- Week 3 — Workshop 1: Formalization of mathematics in proof assistants, organized by Georges Gonthier and Vladimir Voevodsky.
- Week 6 — Workshop 2: Constructive mathematics and models of type theory, organized by Thierry Coquand and Thomas Streicher.
- Week 8 — Workshop 3: Semantics of proofs and programs, organized by Thomas Ehrhard and Alex Simpson.
- Week 10 — Workshop 4: Abstraction and verification in semantics, organized by Paul-André Melliès and Luke Ong.
- Week 12 — Workshop 5, Certification of high-level and low-level programs organized by Christine Paulin and Zhong Shao.

A lot of people I know will attend parts of this, such as Jean Benabou, Marcelo Fiore, Dan Ghica, André Joyal, Samuel Mimram, and Bas Spitters. And that makes me happy, because Paul-André Melliès has invited me to spend up to a month attending this series of workshops, perhaps in two 2-week stretches. With a little luck I’ll be able to actually do this.

(My wife Lisa Raphals has gotten invited to Erlangen for the spring of 2014, meaning roughly April 1 - June 1. If she and I succeed in getting leaves of absence, I’ll go with her, and then take some trips to nearby places. Since I split my time between the Wild West and the Far East, Paris seems nearby to Erlangen to me. I also have vague invitations to IHES, Prague and Berlin which I might try to take advantage of. And if you have a luxurious villa in northern Italy or the French Riviera, let me know.)

## Re: Semantics of Proofs in Paris

This seems oddly

à proposgiven the number of reasonably recent posts on “The current King of France is bald”. ;)