Gallery

One main ambition of my work is to understand how formal proofs should be written down. This simple question is related to a myriad of fascinating problems at the interface of proof theory, games semantics, n-dimensional algebra, and mathematical physics.

For instance, I like to think that « game semantics » is not just another « semantics » for proofs. I prefer to see it as a « syntax ». Of course, this « game syntax » is a new kind of syntax, which does not look like the previous ones -- especially if one thinks of Frege's ideography, Gentzen's sequent calculus, or even Girard's proof-nets.

This new brand of diagrammatic syntax is at the same time a « combinatorics » of proofs, akin to the familiar structure of topological knots in mathematics. The wonderful thing is that we have at our disposal, today, a large amount of tools coming from algebra and mathematical physics, to analyze that kind of diagrammatic situation.

I am confident that this point of view will deeply transform Proof Theory as well as Programming Language Semantics. There are also good reasons to believe that this fresh air coming from algebra and mathematical physics will not be confined to Proof Theory: it should also benefit the other fields of mathematical logic.

Here, I will limit myself to showing you a few diagrams which I have drawn in my work. Some of them describe proofs, others describe structures of connectives or modalities. I have decided to show them here mainly to entertain my non-mathematician friends. However, I will briefly indicate to the specialist reader what kind of mathematical structures are depicted below.

A proof in string diagrams This is the proof that the conjunction of the double negations of two formulas A and B implies the double negation of the conjunction of the two formulas. Note that the trajectories of the negations R and L coincide with the strategy associated to the proof in « game semantics ».

Modalities as boxes I like to draw modalities as boxes, surrounding proofs: intuitively, the modality encapsulates the proof, and indicates a modal attitude to the external world. Interestingly, these modal boxes have a clear algebraic meaning: they model various kinds of (monoidal) functors between (monoidal) categories. I use this diagrammatic language to describe how a proof duplicates another proof in linear logic. This leads to nice diagrams, as this one above, describing a contraction node interacting with the principal door of an exponential box in linear logic. The methodology extends quite nicely to broader territories -- leading to natural extensions of flowchart diagrams in programming language design.

The structure of recursion Martin Hyland and Masahito Hasegawa have shown around 1996 that this construction defines a (parametric) fixpoint operator in any cartesian category with a trace operator -- typically, the category of Scott domains and continuous functions. This amounts to showing that the diagram above is equal to the diagram below. The structure of logical implication The diagram shows that every adjunction does not simply define a monad, but in fact what I like to call a «parametric monad ». This structure captures precisely the property of a logical implication defined by negative translation -- as in the case of language defined by continuations. Associativity of the parametric monad is established thanks to a series of diagrams, involving this one: Monoidal fibrations in string diagrams I have been thinking for a long time at the question of defining a properly fibered version of linear logic and other monoidal proof systems --- and more specifically tensor logic which underlies traditional game semantics. The most natural way to proceed is to start from the usual notion of fibration, and to observe that its algebraic structure may be depicted in the 2-dimensional language of string diagrams. For instance, the diagram above describes the natural transformation which enables to compose together two fiber functors. In order to define the relevant version of monoidal fibration, it is important to remember the lessons of proof systems like separation logic, and to resist the (extremely bad) temptation to ask that every fiber is a monoidal category. Indeed, the idea behind such a fibration is that a program uses the computational resource offered by its fiber (typically a set of allocated memory cells). Hence the tensor product of two programs should live inside the tensor product of their two fibers, because this tensor product is precisely the resource they need in order to achieve their task. This line of thought leads to a very natural notion of monoidal fibration, which requires to shift from the language of string diagrams to the 3-dimensional language of surface diagrams. For instance, the diagram above depicts the natural transformation which enables to tensor together two independent fiber functors.

The notion of monoidal fibration is extremely natural... but strangely enough I was not able to find the notion in the literature for a very long time. It is only a few years ago that I discovered it with great excitement (and relief!) in this article written by Mike Shulman --- where the notion of monoidal fibration which I had in mind is formulated and studied from several angles.

Random walks on configuration spaces

This applet computes a random walk on the configuration space of an event structure of 12 × 12 × 12 little cubes. The random walk is carefully designed in order to converge to the uniform distribution on the set of configuration spaces. To that purpose, it follows the Glauber dynamics associated to the distribution. If you are sufficiently patient, you will see that the walk eventually reaches a random sample where something like an artic circle separates a liquid phase and a solid phase.

The very same story as above, but this time on a grid of 25 × 25 × 25 little cubes, or even 50 × 50 × 50 little cubes, depending on your taste and appetite.