Rencontre, 16 novembre 2023
Programme
- 10:30 – 12:00
-
Morgan Rogers (LIPN, Université Sorbonne Paris-Nord)Invited talk: A topos theory travel guide
Topos theory can be a little intimidating: it's a vast subject with a lot of baggage attached, and like many areas of category theory you need to be prepared to go quite deep to be rewarded. Unfortunately, that entry barrier makes the subject almost inaccessible to a casual reader! In this talk, I will help you get your head around the jargon. What is a subobject classifier? What is the difference between an elementary topos and a Grothendieck topos? Where do sheaves come in and what are they, anyway? How are these generalized spaces? What is a classifying topos? What's the internal language? Nominal sets form some kind of topos, right? What about infinity-toposes? Armed with this knowledge and a bunch of examples, you'll stand a better chance of figuring out how to make toposes work for you.
For the uninitiated, I will spend the first 15 minutes or so introducing category theory through some examples (which may miraculously turn out to be toposes). I don't expect to have a lot of time for non-examples, but I am happy to field questions. I also don't know in advance whether I will be able to cover everything I wrote above, but I will try my best.
(note for people following at a distance: the talk will be given on a blackboard)
- 13:45 – 14:45
-
Cyril Cohen (INRIA)
Libraries of formalized mathematics use a possibly broad range of different representations for a same mathematical concept. Yet light to major manual input from users remains most often required for obtaining the corresponding variants of theorems, when such obvious replacements are typically left implicit on paper. This talk presents Trocq, a new proof transfer framework for dependent type theory. Trocq is based on a novel formulation of type equivalence, used to generalize the univalent parametricity translation. This framework takes care of avoiding dependency on the axiom of univalence when possible, and may be used with more relations than just equivalences. We have implemented a corresponding plugin for the Coq proof assistant, in the CoqElpi meta-language. We use this plugin on a gallery of representative examples of proof transfer issues in interactive theorem proving, and illustrate how Trocq covers the spectrum of several existing tools, used in program verification as well as in formalized mathematics in the broad sense.
Joint work with Enzo Crance and Assia Mahboubi.
- 15:15 – 16:15
-
Simon Forest (Université Aix-Marseille)
Thin spans were recently introduced as a quantitative, or proof-relevant, model of programming languages based on spans of groupoids. As a model of linear logic, they can be seen as an extension of the relational model Rel where, in the interpretation of a program, not only some inputs are related to some outputs, but the different ways or computations a program can make to transform the given inputs to the given outputs are recorded.
In an ongoing work, we show that thin spans provide a useful model of so-called rigid intersection types, that are non-idempotent and non-commutative intersection types. It is already known that the relational model Rel can be syntactically described using a non-idempotent but commutative intersection type system. The commutativity is essential for the property of subject reduction, stating that the interpretation of a program is not changed by reduction. Nevertheless, the interpretation of programs in thin spans can be described by a rigid intersection type system, while still enjoying a relaxed subject reduction property.
In this talk, a rather light-weight presentation of thin spans will be given, followed by a presentation of the rigid intersection type system associated to them.
This is joint work with Pierre Clairambault.
