On Friday the 3rd of May, at 10am, I will give a talk on “Deductive systems and Grothendieck topologies” at the seminar of the research group Deducteam of the École normale supérieure Paris-Saclay.

In the talk I will show that the classical proof system of geometric logic over a given geometric theory is equivalent to new proof systems based on the notion of Grothendieck topology. Remarkably, these new systems, which are related to the classsical one through topos-theoretic ‘bridges’, are computationally much better-behaved for many purposes, as I will illustrate by discussing a few notable applications.

We are looking forward to a computer implementation of these techniques allowing to exploit all the computational advantages deriving from the multiplication of points of view which is made possible by topos theory.

You can attend the talk in presence (in Room 1Z71 of the ENS Paris-Saclay) or online, at this Zoom link.

More information is available at the seminar page.

Looking forward to seeing many of you there!