Seminars

Proofs and Models in the TPTP World

Was on 11 July 2024.

Geoff Sutcliffe (University of Miami)

This talk describes the representation of proofs and models in the TPTP World. Topics covered include the TPTP World, the TPTP language, the SZS ontologies, the representation of proofs and models, tools for visualizing and verifying proofs and models, and current work using Dedukti to verify derivations.

Deducteam Intern Day

Was on 11 July 2024.

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.

PhD Defence: Prétraitement compositionnel en Coq

Was on 10 July 2024.

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.

Jury :

• Sylvain Boulmé, Rapporteur & Examinateur, Maître de Conférences, Université Grenoble-Alpes
• Nicolas Tabareau, Rapporteur & Examinateur, Directeur de Recherche, INRIA
• Sylvie Boldo, Examinatrice, Directrice de Recherche, INRIA
• Sophie Tourret, Examinatrice, Chargée de Recherche, INRIA
• Yannick Forster, Invité, Chargé de Recherche, INRIA

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.