Unless stated otherwise, seminars take place at LMF, ENS Paris-Saclay, 4 avenue des Sciences, 91190 Gif-sur-Yvette, France. Please ask ahead of time if you want to attend online. To stay informed, you can subscribe to our mailing list.
Access the list of seminars from before 2024.Deducteam Intern Day
On 11 July 2024, at 10:45, in room 1Z28.
Interns (Deducteam)
The interns of our team will each give a talk about their respective ongoing internship.
This day will be preceded by Geoff Sutcliffe's talk at 9:30.
| Time | Name |
|---|---|
| 9:30 — 10:30 | Geoff Sutcliffe |
| 10:45 — 11:30 | Intern 1 |
| 11:30 — 12:15 | Intern 2 |
| 12:15 — 13:30 | Lunch |
| 13:45 — 14:30 | Intern 3 |
| 14:30 — 15:15 | Intern 4 |
TBA
On 11 July 2024, at 9:30, in room 1Z28.
Geoff Sutcliffe (University of Miami)
TBA
PhD Defence: Prétraitement compositionnel en Coq
On 10 July 2024, at 14:00, in room 1Z31.
Louise Dubois de Prisque (LMF)
Louise will defend her PhD thesis, in French.
Le manuscrit, en français également, est sur ma page web : https://louiseddp.github.io/.
Cette thèse présente une nouvelle méthodologie de prétraitement de buts de l'assistant de preuve Coq afin de les envoyer à un prouveur automatique. Cette méthodologie consiste à composer des transformations atomiques et certifiantes en fonction du but à prouver. Nous présenterons d'abord la bibliothèque de transformations que nous avons écrite, puis nous présenterons un outil d'ordonnancement pour ces transformations, qui se veut générique. Le tout a conduit à l'implémentation une nouvelle tactique 'pousse-bouton' appelée 'snipe' pour Coq.
Generalized Set Theories in Higher-Order Logic
Was on 6 June 2024.
Ciarán Dunne (LMF)
Set theories like Zermelo-Fraenkel (ZF) and Tarski-Grothendieck (TG) are "foundations of mathematics"; they provide a formal conception of set that is powerful and flexible enough for encoding a plethora of mathematical objects. When a set theory is used as the logical foundation of a proof assistant, nearly all mathematical objects have the same type, namely the type set. In contrast, many widely used proof assistants rely crucially on approaches where mathematical objects are organised into a vast number of types.
A generalized set theory (GST) is similar to a standard set theory, but allows having mathematical objects like pairs, functions, ordinals, etc., as objects that are not sets. Within a GST, all objects have the same (syntactic) type, but are partitioned into many soft types, which simulate some of the benefits of type theory.
In this talk, we explore the axiomatization and model construction techniques for GSTs in higher-order logic, and the implementation of both of these aspects in Isabelle/HOL.
Deductive systems and Grothendieck topologies
Was on 3 May 2024.
Olivia Caramello (University of Insubria, Como)
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. These equivalences result from a proof-theoretic interpretation of the duality between the quotients of a geometric theory and the subtoposes of its classifying topos. Interestingly, these new proof systems turn out to be computationally better-behaved than the classical one for many purposes, as I will illustrate by discussing a few selected applications.
Trocq: Proof Transfer for Free, With or Without Univalence
Was on 12 January 2024.
Enzo Crance (Gallinette, Inria Rennes, LS2N, Mitsubishi Electric)
Formalisation projects make use of a possibly broad range of different representations for a same mathematical concept. Yet, substantial manual input often remains necessary to switch from a representation to another, even though it is typically left implicit on paper. In this talk, we will present Trocq, a new proof transfer framework for dependent type theory. It is based on a generalisation of univalent parametricity, able to avoid dependency on the univalence axiom when possible, and able to exploit more relations that just equivalences. We will also present the implementation of Trocq, a plugin for the Coq proof assistant, written using the Coq-Elpi meta-language.
Fixed Point Theorems for Non-Transitive Relations
Was on 10 January 2024.
Jérémy Dubut-Kross (AIST, Tokyo)
We develop an Isabelle/HOL library of order-theoretic fixed-point theorems. We keep our formalization as general as possible: we reprove several well-known results about complete orders, often with only antisymmetry or attractivity, a mild condition implied by either antisymmetry or transitivity. In particular, we generalize various theorems ensuring the existence of a quasi-fixed point of monotone maps over complete relations, and show that the set of (quasi-)fixed points is itself complete. This result generalizes and strengthens theorems of Knaster-Tarski, Bourbaki-Witt, Kleene, Markowsky, Pataraia, Mashburn, Bhatta-George, and Stouti-Maaden.
Joint work with Akihisa Yamada.