Seminars

Strict Categories with Families

Was on 26 November 2024.

Loïc Pujet (University of Stockholm)

Categories with families (CwF) are perhaps the most widely used notion of models for dependent types. They can be described by an algebraic signature with dependent sorts for contexts, substitutions, types and terms, as well as a plethora of constants and equations. Unfortunately, this mix of dependent sorts and equations is particularly prone to transport hell, and in practice it is nearly impossible to prove non-trivial results using CwFs in a proof assistant.

In this talk, I will present a method based on Pédrot's "prefascist sets" to strictify (nearly) all the equations of a CwF, so that they hold by definition. I will then discuss applications of this method to formal proofs of canonicity and normalisation.

This is joint work with Ambrus Kaposi.

Towards a Type System for SMT-LIB v3

Was on 7 November 2024.

Ciarán Dunne (LMF)

The specification language SMT-LIB is the input language for SMT-solvers. Scripts in the SMT-LIB v2.6 represent configurations in many-sorted first-order logic (MFOL). A preliminary proposal for SMT-LIB v3 contemplates a significant shift from the traditional first-order setup to a higher-order logic with dependent types.

In this talk, we argue that the calculus of constructions (CC) is a suitable candidate for the abstract syntax of SMT-LIB v3. In particular, we demonstrate how concrete SMT instances, theories, and proofs can be interpreted in CC.

Moreover, we build on the work of Barras to give classical, set-theoretic semantics to our abstract syntax and make precise the central notion of satisfiability for SMT-LIB v3.

Finally, we will sketch out the details of how this interpretation can be leveraged to use Dedukti as a type-checker (and hence a proof-checker) for SMT-LIB v3.

Generation and automation of identity proofs in dependent type theory.

Was on 17 October 2024.

Thibaut Benjamin (University of Cambridge)

Dependent type theory based proof assistants are one of the tools offering the strongest guarantees on a software. However, in practical large scale project they induce a heavy proof effort, limiting their adoption. A common situation is that of a program using efficient datatypes, that lend themselves poorly to reasoning, making proofs very technical. A potential solution relies on the univalence principle proposed by Voevodski, stating that the correct notion of equality between datatypes is that of isomorphism. This allows one to transport programs and proofs on easy-to-reason-with but computationally inefficient datatypes to efficient ones. Unfortunately this principle is incompatible with that of uniqueness of identity proofs (UIP), another principle that is used to simplify reasoning. In practice, this means that reasoning under univalence requires one to carefully handle identity proofs, which is tricky. In this talk, I will present my work and a research direction allowing to simplify the handling of identity proofs. It relies on a tool I am developing called CaTT, allowing one to work in the algebraic structure of the identity types. I will show how the work in this tool can be partially automated, and I will demonstrate a Coq plug-in letting one generate computations on identity terms. This reduces the proof effort to manage identity types. Moreover, the incompatibility between the two principles entails that it is not sound to simultaneously use results from a library requiring univalence and from one requiring UIP. In practice though, some uses of UIP are superfluous, and it is sometimes possible to make the two library compatibles. The work I will present gives a hint towards a way to understand exactly when this is possible, and the degree of human intervention needed to do it.

The Max-Atom Problem applied to Universe Polymorphism in Type Theory

Was on 19 September 2024.

Marc Bezem (Universitetet i Bergen)

We give a short introduction to the Max-Atom Problem and its connection to type theory. Then we generalize to join-semilattices with an inflationary endomorphism and we explain how this generalization can be reformulated with Horn clauses (using an idea of Lorenzen). The key problems connected to universe polymorphism in type theory can now be formulated as loop checking problems and uniform word problems for this kind of lattices. Both can be solved by the computation of least Herbrand models of the corresponding Horn clauses.

In the second half of the talk we propose a type theory with explicit universe polymorphism, featuring level-indexed product types and constraint-indexed product types. In this type theory, loop checking and uniform word problems in the above mentioned lattices play a crucial role.

Efficiency and complexity issues will briefly be addressed throughout the talk. The research presented here is joint work with many people: Nieuwenhuis, Rodríguez-Carbonell, Coquand, Dybjer, Escardó.

PhD Defence: Generic Bidirectional Typing in a Logical Framework for Dependent Type Theories

Was on 18 September 2024.

Thiago Felicissimo (LMF)

Thiago will defend his PhD thesis.

The current version of the manuscript can be found here.

Abstract

Dependent type theories are formal systems that can be used both as programming languages and for the formalization of mathematics, and constitute the foundation of popular proof assistants such as Coq and Agda. In order to unify their study, Logical Frameworks (LFs) provide a unified meta-language for defining such theories in which various universal notions are built in by default and metatheorems can be proven in a theory-independent way.

This thesis focuses on LFs designed with implementation in mind, with the goal of providing generic type-checkers. Our main contribution is a new such LF which allows for representing type theories with their usual non-annotated syntaxes. The key to allowing the removal of annotations without jeopardizing decidability of typing is the integration of bidirectional typing, a discipline in which the typing judgment is decomposed into inference and checking modes. While bidirectional typing has been well known in the literature for quite some time, one of the central contributions of our work is that, by formulating it in an LF, we give it a generic treatment for all theories fitting our framework. Our proposal has been implemented in the generic type-checker BiTTs, allowing it to be used in practice with various theories.

In addition to our main contribution, we also advance the study of Dedukti, a sibling LF of our proposed framework. First, we revisit the problem of showing that theories are correctly represented in Dedukti by proposing a methodology for encodings which allows for showing their conservativity easily. Furthermore, we demonstrate how Dedukti can be used in practice as a tool for translating proofs by proposing a transformation for sharing proofs with predicative systems. This transformation has allowed for the translation of proofs from Matita to Agda, yielding the first-ever Agda proofs of Fermat's Little Theorem and Bertrand's Postulate.

Members of the jury:

• Andrej Bauer, University of Ljubljana - Reviewer
• Herman Geuvers, Radboud University Nijmegen - Reviewer
• Marc Bezem, University of Bergen
• Christine Paulin-Mohring, Université Paris-Saclay
• Temur Kutsia, Johannes Kepler University Linz
• Frank Pfenning, Carnegie Mellon University
• Frédéric Blanqui, Inria Saclay - Supervisor
• Gilles Dowek, Inria Saclay & ENS Paris-Saclay - Supervisor

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.

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.

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.