2024Activity reportProject-TeamDEDUCTEAM

6.1.1 Lambdapi

• Keywords:
  Dependent types, Rewriting, Proof assistant
• Functional Description:

  Lambdapi is an interactive proof development system featuring dependent types like in Martin-Lőf’s type theory, but allowing to define objects and types using oriented equations, aka rewriting rules, and reason modulo those equations. This allows to simplify some proofs, and formalize complex mathematical objects that are otherwise impossible or difficult to formalize in more traditional proof systems.

  Lambdapi comes with Emacs and VSCode support.

  Lambdapi can also read and output Dedukti files, and can thus be used as an higher-level intermediate language for translating proofs from one system to Dedukti.

  Lambdapi is a logical framework and does not come with a pre-defined logic. However, it is easy to define a logic by declaring a few symbols and rules. A library of pre-defined logic is also provided.

  Here are some of the features of Lambdapi: - Emacs and VSCode plugins (based on LSP) - support for unicode (UTF-8) and user-defined infix operators - symbols can be declared commutative, or associative and commutative - some arguments can be declared as implicit: the system will try to find out their value automatically - symbol and rule declarations are separated so that one can easily define inductive-recursive types or turn a proved equation into a rewriting rule - support for interactive resolution of typing goals, and unification goals as well, using tactics - a rewrite tactic similar to the one of SSReflect in Coq - the possibility of calling external automated provers - a command is provided for automatically generating an induction principle for (mutually defined) strictly-positive inductive types - Lambdapi can call external provers for checking the confluence and termination of user-defined rewriting rules by translating them to the XTC and HRS formats used in the termination and confluence competitions

• URL:
  https://­github.­com/­Deducteam/­lambdapi
• Contact:
  Frederic Blanqui

6.1.2 Dedukti

• Keyword:
  Logical Framework
• Functional Description:

  Dedukti is a proof-checker for the LambdaPi-calculus modulo. As it can be parametrized by an arbitrary set of rewrite rules, defining an equivalence relation, this calculus can express many different theories. Dedukti has been created for this purpose: to allow the interoperability of different theories.

  Dedukti's core is based on the standard algorithm for type-checking semi-full pure type systems and implements a state-of-the-art reduction machine inspired from Matita's and modified to deal with rewrite rules.

  Dedukti's input language features term declarations and definitions (opaque or not) and rewrite rule definitions. A basic module system allows the user to organize his project in different files and compile them separately.

  Dedukti features matching modulo beta for a large class of patterns called Miller's patterns, allowing for more rewriting rules to be implemented in Dedukti.

• URL:
  https://­deducteam.­github.­io/
• Publications:
  hal-01086609, hal-01176715, hal-01441751
• Contact:
  Frederic Blanqui
• Participants:
  Francois Thire, Gaspard Ferey, Guillaume Genestier, Rodolphe Lepigre

6.1.3 hol2dk

• Keywords:
  Interoperability, Proof
• Functional Description:
  Tool making HOL-Light generate proofs, simplifying those proofs, and translating those proofs to Dedukti, Lambdapi and Coq.
• URL:
  https://­github.­com/­Deducteam/­hol2dk
• Contact:
  Frederic Blanqui

6.1.4 BiTTs

• Keywords:
  Dependent types, Logical Framework
• Functional Description:
  This is an implementation of the generic bidirectional typing algorithm presented in the paper "Generic bidirectional typing for dependent type theories".
• URL:
  https://­github.­com/­thiagofelicissimo/­BiTTs
• Contact:
  Thiago Felicissimo Cesar

6.1.5 Predicativize

• Name:
  Predicativize
• Keywords:
  Dedukti, Proof assistant, Interoperability
• Functional Description:
  Predicativize is a tool allowing for the translation of proofs from a core impredicative type theory to a core predicative theory featuring universe polymorphism. It works by calculating constraints between universe levels, which are then solved using universe level unification, generating then a predicative universe polymorphic definition. The theory behind the tool is provided in the paper "Translating proofs from an impredicative type system to a predicative one", by Thiago Felicissimo, Frédéric Blanqui and Ashish Kumar Barnawal. Predicativize was used to translate Matita's arithmetic library to Agda.
• URL:
  https://­github.­com/­Deducteam/­predicativize
• Contact:
  Thiago Felicissimo Cesar

6.1.6 commutative-diagrams

• Name:
  Commutative diagrams proof assistant
• Keyword:
  Proof assistant
• Functional Description:
  A coq plugin enabling to progress categoretical proofs graphically. It can infer the diagram from the proof context, and display it graphically to the user. The user's action on the diagram are then converted into Coq proofs.
• URL:
  https://­github.­com/­dwarfmaster/­commutative-diagrams
• Contact:
  Luc Chabassier

6.1.7 pogtranslator

• Keywords:
  Formal methods, Proof
• Functional Description:
  Translator of Atelier B proof obligations (in the POG format) to the TPTP or SMT-LIB format.
• Contact:
  Claude Stolze

6.1.8 sniper

• Keywords:
  Coq, Automated deduction
• Functional Description:
  Sniper is a Coq plugin that improves its automation.
• URL:
  https://­github.­com/­smtcoq/­sniper
• Contact:
  Chantal Keller
• Partner:
  Université Paris-Saclay

6.1.9 dkpltact

• Keywords:
  Coq, Interoperability, Proof
• Functional Description:
  A tool to translate proofs from a Dedukti encoding of Predicate logic to the tactic language of Coq. It takes Dedukti files whose terms comply with this encoding and produces the corresponding Coq files.
• URL:
  https://­gitlab.­crans.­org/­geran/­dkpltact
• Contact:
  Yoan Geran

6.1.10 Zenon Modulo

• Keywords:
  First-order logic, Automated theorem proving, Deduction Modulo
• Functional Description:
  Zenon Modulo is an extension of the automated theorem prover Zenon. Compared to Super Zenon, it can deal with rewrite rules both over propositions and terms. Like Super Zenon, Zenon Modulo is able to deal with any first-order theory by means of a similar heuristic.
• URL:
  https://­github.­com/­Deducteam/­zenon_modulo
• Contact:
  Guillaume Burel
• Partner:
  ENSIIE

6.1.11 Agda2Dedukti

• Keywords:
  Compilation, Proof assistant, Higher-order logic, Rewriting systems
• Functional Description:
  Translation of Agda proofs to the Logical Framework Dedukti.
• URL:
  https://­github.­com/­Deducteam/­Agda2Dedukti
• Contact:
  Thiago Felicissimo Cesar
• Partner:
  Chalmers University

6.1.12 Coqine

• Name:
  Coq In dEdukti
• Keywords:
  Higher-order logic, Formal methods, Proof
• Functional Description:
  CoqInE is a plugin for the Coq software translating Coq proofs into Dedukti terms. It provides a Dedukti signature file faithfully encoding the underlying theory of Coq (or a sufficiently large subset of it). Current development is mostly focused on implementing support for Coq universe polymorphism. The generated ouput is meant to be type-checkable using the latest version of Dedukti.
• URL:
  http://­www.­ensiie.­fr/­~guillaume.­burel/­blackandwhite_coqInE.­html.­en
• Contact:
  Guillaume Burel

6.1.13 Krajono

• Keyword:
  Proof
• Functional Description:
  Krajono translates Matita proofs into Dedukti[CiC] (encoding of CiC in Dedukti) terms.
• Contact:
  Claudio Sacerdoti Coen

6.1.14 personoj

• Keywords:
  PVS, Automated theorem proving, Dedukti, Machine translation
• Functional Description:
  Personoj comprises a set of PVS patches that may be used to export PVS specifications (propositions and definitions) or to export successive sequents of a proof to lambdapi. Another program is able to process these sequents and call automated theorem provers through Why3 to prove the implications of the successive sequents.
• Contact:
  Gabriel Hondet

6.1.15 Holide

• Keyword:
  Proof
• Functional Description:
  Holide translates HOL proofs to Dedukti[OT] proofs, using the OpenTheory standard (common to HOL Light and HOL4). Dedukti[OT] being the encoding of OpenTheory in Dedukti.
• URL:
  https://­github.­com/­Deducteam/­Holide
• Contact:
  Guillaume Burel

6.1.16 Logipedia

• Name:
  Logipedia
• Keywords:
  Formal methods, Web Services, Logical Framework
• Functional Description:

  Logipedia is composed of two distinct parts: 1) A back-end that translates proofs expressed in a theory encoded in Dedukti to other systems such as Coq, Lean or HOL 2) A front-end that prints these proofs in a "nice way" via a website. Using the website, the user can search for a definition or a theorem then, download the whole proof into the wanted system.

  Currently, the available systems are: Coq, Matita, Lean, PVS and OpenTheory. The proofs comes from a logic called STTForall.

  In the long run, more systems and more logic should be added.

• Release Contributions:
  This is the beta version of Logipedia. It implements the functionalities mentioned above.
• URL:
  http://­www.­logipedia.­science
• Contact:
  Frederic Blanqui

6.1.17 SKonverto

• Name:
  SKonverto
• Keywords:
  Skolemization, First-order logic, Proof assistant
• Functional Description:
  SKonverto is a tool that transforms Lambdapi proofs containing Skolem symbols into proofs without these symbols.
• URL:
  https://­github.­com/­Deducteam/­SKonverto
• Contact:
  Mohamed Yacine El Haddad
• Partner:
  ENSIIE

HOL-Light definition of number types in Coq

• Project link:
  https://­github.­com/­Deducteam/­coq-hol-light-real
• Contact:
  Frédéric Blanqui

Translation of HOL-Light base library to Coq

• Project link:
  https://­github.­com/­Deducteam/­coq-hol-light
• Contact:
  Frédéric Blanqui

Translation of Matita arithmetic library to Agda

• Project link:
  https://­github.­com/­Deducteam/­matita_lib_in_agda
• Contact:
  Thiago Felicissimo

7.1.1 Ghost types and equality reflection

Participants: Ewen Broudin–Caradec, Théo Winterhalter.

We introduced ghost type theory (GTT) a dependent type theory extended with a new universe for ghost data that can safely be erased when running a program but which is not proof irrelevant like with a universe of (strict) propositions. Instead, ghost data carry information that can be used in proofs or to discard impossible cases in relevant computations. Casts can be used to replace ghost values by others that are propositionally equal, but crucially these casts can safely be ignored for conversion. We provide a type-preserving erasure procedure which gets rid of all ghost data and proofs, a step which may be used as a first step to program extraction. We give a syntactical model of GTT using a program translation akin to the parametricity translation and thus show consistency of the theory. Because it is a parametricity model, it can also be used to derive free theorems about programs using ghost code. We further extend GTT to support equality reflection and show that we can eliminate its use without the need for the usual extra axioms of function extensionality and uniqueness of identity proofs. In particular we validate the intuition that indices of inductive types—such as the length index of vectors—do not matter for computation and can safely be considered modulo theory. Our results have been formalised in Coq and lead to a POPL publication 18.

7.1.2 Type preserving rewrite rules for the Coq proof assistant

Participants: Théo Winterhalter.

We present an implementation of rewrite rules on top of the Coq proof assistant, together with a modular criterion to ensure that the added rewrite rules preserve typing. This criterion, based on bidirectional type checking, is formally expressed in the type theory of Coq. This lead to an ITP publication 28.

7.1.3 Generic bidirectional typing for dependent type theories

Participants: Thiago Felicissimo, Frédéric Blanqui, Gilles Dowek.

Bidirectional typing is a discipline in which the typing judgment is decomposed explicitly into inference and checking modes, allowing to control the flow of type information in typing rules and to specify algorithmically how they should be used. Bidirectional typing has been fruitfully studied and bidirectional systems have been developed for many type theories. However, the formal development of bidirectional typing has until now been kept confined to specific theories, with general guidelines remaining informal. In this work, we give a generic account of bidirectional typing for a general class of dependent type theories. This is done by first giving a general definition of type theories (or equivalently, a logical framework), for which we define declarative and bidirectional type systems. We then show, in a theory-independent fashion, that the two systems are equivalent. This equivalence is then explored to establish the decidability of typing for weak normalizing theories, yielding a generic type-checking algorithm that has been implemented in a prototype and used in practice with many theories. This work was published at ESOP 24 and an extended version has been accepted for publication at TOPLAS.

7.1.4 Second-order Church-Rosser modulo, without normalization

Participants: Thiago Felicissimo.

Rewriting modulo is an alternative to standard rewriting in which one considers not only rewriting rules but also undirected equations, allowing to handle theories defined by axioms that cannot be oriented in a well-behaved manner, such as commutativity. In this setting, the Church-Rosser property must be adapted into Church-Rosser modulo. Unfortunately, most criteria for Church-Rosser modulo rely on normalization, yet confluence proofs for dependent type theories are usually carried out on untyped terms, for which normalization does not hold due to rules such as $\beta$-reduction. In this work, we investigate criteria for proving Church-Rosser modulo of second-order rewrite systems without relying on normalization. This work was published at IWC 25.

7.4.1 Impredicativity, cumulativity and product covariance in Dedukti

Participants: Thiago Felicissimo, Théo Winterhalter.

Proof assistants such as Coq implement a type theory featuring three important features: impredicativity, cumulativity and product covariance. This combination has proven difficult to be expressed in Dedukti, and previous attempts have failed in providing an encoding that is proven confluent, sound and conservative. We solve this longstanding open problem by providing an encoding of these three features that we prove to be confluent, sound and to satisfy a restricted (but, we argue, strong enough) form of conservativity. Our proof of confluence is a contribution by itself, and combines various criteria and proof techniques from rewriting theory. Our proof of soundness also contributes a new strategy in which the result is shown in terms of an inverse translation function, fixing a common flaw made in previous encoding attempts. This work was published at FSCD 26.

7.4.2 A linear Rewrite System to Represent Impredicative and Cumulative Universes with Polymorphism

Participants: Yoan Géran.

Yoan Géran has designed a rewrite system to represent, in the $\lambda \Pi$-calculus modulo theory, type universes that feature cumulativity, impredicativity of the first universe, and universe polymorphism. This system extends previous works and is now confluent, terminating, and left-linear.

7.4.3 Translating Lean to Dedukti

Participants: Rishikesh Vaishnav, Frédéric Blanqui.

This year, Rishikesh Vaishnav made progress on various aspects of the translation from Lean to Dedukti. Notably, he completed the implementation of instantiation scheme for universe level variables in lean2dk (work that was started last year in collaboration with Yoan Geran), extended the translation to handle more cases of definitional equality/reduction, and started to attempt the translation of Lean's standard library's prelude files. In doing so, he identified some tricky cases of definitional equality that are difficult to encode, in particular Lean's support for K-like reduction and proof irrelevance. This prompted an investigation into the possibility of pre-translating Lean into a smaller theory that replaces these definitional rules with axioms in order to ease translation, resulting in the implementation of the tool "Lean4Less" (see section 7.5.1).

7.4.4 Making Leo-III output Lambdapi proofs

Participants: Melanie Taprogge, Frédéric Blanqui.

Melanie Taprogge began her PhD in October, building on the work from her Master thesis 38. Her project focuses on certifying the proofs generated by the fully automated higher-order logic theorem prover Leo-III through an encoding of its proofs in Lambdapi. She analyzed the particular challenges involved in this encoding and developed strategies to address them. This effort resulted in a general schema that can be systematically applied to encode inference rules and their applications, both for Leo-III and other automated systems. The effectiveness of this approach was demonstrated by deriving encodings for some core inference rules of the EP calculus implemented in Leo-III, as well as a partial implementation of the proof output, yielding a verifiable proof of a popular benchmark problem for testing the capabilities of automated reasoning systems. In collaboration with team members working on the expression of other proof systems in Lambdapi, particularly Alessio Coltellacci, Anne Grieu, Ciarán Dunne and Frédéric Blanqui, Melanie identified several encodings necessary across different projects that had previously been addressed using different strategies in each project. She contributed to the development of more general encodings of such principles, aiming for a more uniform and widely applicable representation across multiple projects and systems.

7.4.5 Translating Eunoia to Dedukti and Lambdapi

Participants: Ciarán Dunne, Guillaume Burel.

Ciarán has been working towards the development of a tool named eo2dk for automated translation of specifications and proofs of the Eunoia logical framework to Dedukti and Lambdapi. Eunoia (formerly AletheLF) is a dependently-typed logical framework designed for specifying the theories and proof systems used by SMT solvers (in particular, cvc5). Among other features, Eunoia extends the core SMT-LIB language with dependent types (with implicit paramters), rewrite rules, and a mechanism for defining inference rules.

Currently, the only proof system defined in Eunoia is cvc5's co-operating proof calculus (CPC). First, our translation tool will allow automatically translating the inference rules of CPC to a library of symbol declarations in Dedukti. In turn, the proofs outputted by cvc5 can be translated into Dedukti proof terms using those symbols. All together, we provide an external proof-checker for cvc5 that can be easily updated as the rules of CPC inevitably change.

Furthermore, we have developed a set-theoretic semantics of Eunoia based on the types-as-sets interpretation given by Aczel, Werner and Barras. The aim of this work is gain a understanding of dependently-typed extensions of SMT-LIB 2 (like Eunoia, and the anticipated release of SMT-LIB v3), and to also lay the groundwork for verifying the soundness of the encoding used in eo2dk.

7.4.6 Translating B Proof Obligations to Dedukti

Participants: Claude Stolze, Olivier Hermant.

In the framework of the ICSPA ANR project, Claude Stolze has implemented a translator from B proof obligations to why pog3why. The intermediate translation to Why3 allowed to use automated theorem provers on the proofs obligations 35 (joint work with Romain Guillaumé).

7.4.7 Translating Dedukti proofs to Coq with Tactics

Participants: Yoan Geran.

Yoan Géran has implemented a translator, dkpltact, for the GeoCoq library embedding in Dedukti,back to Coq. After a reverse mathematical analyzis and a minimization of the embeddding to minimal logic, he translated the library back to Coq by generating proof scripts. This yielded a back-and-forth translation from Coq to Coq with two properties : the logic has been minimized, and the size of the proof scripts/files is not increased.

7.5.1 Implementing a translation from extensional to intensional type theory in Lean

Participants: Rishikesh Vaishnav, Frédéric Blanqui.

In support of his work translating from Lean to Dedukti, Rishikesh Vaishnav implemented an extensional-to-intensional translation framework Lean4Less which is based on a theoretical formalization of an ETT to ITT translation found in ett-to-itt. It implements a specialized case of this translation that replaces uses of definitional proof irrelevance and K-like reduction with type transport using a proof irrelevance axiom, translating Lean to the smaller theory ${\text{Lean}}^{-}$ which should be a better candidate for translation to Dedukti.

In implementing Lean4Less, he added a number of optimizations to help minimize the output size and avoid redundancy. The tool as currently implemented is capable of translating the entirety of the Lean standard library into ${\text{Lean}}^{-}$. Further work remains to be done to scale this translation up to Mathlib. Because this implementation should be consistent with the general ETT to ITT translation, it should also be possible to extend and adapt it for use in Lean's elaboration routine to simulate extensional typechecking in Lean.

A work-in-progress report was presented at LFMTP 2024 37, and a complete publication is targeted for FSCD 2025.

7.5.2 Replacement of rewrite rules by axioms

Participants: Thomas Traversié, Valentin Blot, Gilles Dowek, Théo Winterhalter.

We showed that it is possible to replace the rewrite rules of a theory of the $\lambda \Pi$-calculus modulo theory by equational axioms, when this theory features the notions of proposition and proof, while maintaining the same expressiveness. To do so, we introduced in the target theory a heterogeneous equality, and we built a translation that replaces each use of the conversion rule by the insertion of a transport. At the end, the theory with rewrite rules is a conservative extension of the theory with axioms. This work was published at FoSSaCS 21.

7.5.3 Translation from classical logic to intuitionistic logic

Participants: Thomas Traversié, Olivier Hermant.

In 1951, Kuroda defined an embedding of classical first-order logic into intuitionistic logic, such that a formula and its translation are equivalent in classical logic. Recently, Brown and Rizkallah extended this translation to higher-order logic, but did not prove the classical equivalence, and showed that the embedding fails in the presence of functional extensionality. We proved that functional extensionality and propositional extensionality are sufficient to derive the classical equivalence between a higher-order formula and its translation. We emphasized a condition under which Kuroda’s translation works with functional extensionality. This work was submitted for publication 36.

The next step was to adapt this work to the $\lambda \Pi$-calculus modulo theory and to Dedukti proofs. Kuroda’s translation can be adapted for theories encoded in higher-order logic in the $\lambda \Pi$-calculus modulo theory. As we work with theories—that is with typed constants and rewrite rules—we have to translate them as well. Moreover, we developed a tool Construkti that implements Kuroda’s translation for proofs written in Dedukti. This work was published at LFMTP 29.

Recently, we started working on extending to higher-order logic several translations that generalize double-negation translations by using monad operators instead of double negations. Such translations eliminate particular axioms, for instance the principle of excluded middle or the principle of exclusion, and therefore embed classical logic into intuitionistic logic or intuitionistic logic into minimal logic.

7.5.4 Generic translation templates for Dedukti

Participants: Thomas Traversié.

Since the $\lambda \Pi$-calculus modulo rewriting is used as a formal middleware for exchanging proofs between different proof systems, it is important to define generic translations between theories of the $\lambda \Pi$-calculus modulo rewriting.

To this end, we defined an interpretation of theories of the $\lambda \Pi$-calculus modulo theory, in which a morphism and its invariants are mutually defined. Such an interpretation allows to transfer proofs between theories that feature the notions of proposition and proof, when the source theory can be embedded into the target theory. This work was published in LFMTP 30.

Several translations templates already exist for LF, for instance theory morphisms 41 and logical relations 42, but all of these developments were done in the absence of rewriting. we extended the existing theory morphisms and logical relations to theories of the $\lambda \Pi$-calculus modulo rewriting. We implemented TranslationTemplates these translation templates in Dedukti and formalized some case studies. This work launched a collaboration with Florian Rabe (University of Erlangen).

7.5.5 Translating HOL-Light proofs to Dedukti, Lambdapi and Coq

Participants: Frédéric Blanqui.

In 20, we present a method and a tool, hol2dk, to fully automatically translate proofs from the proof assistant HOL-Light to the proof assistant Coq, by using Dedukti as an intermediate language. Moreover, a number of types, functions and predicates defined in HOL-Light are proved (by hand) to be equal to their counterpart in the Coq standard library. By replacing those types and functions by their Coq counterpart everywhere, we obtain a library of theorems (based on classical logic like HOL-Light) that can directly be used and applied in other Coq developments.

7.5.6 Equivalence of the types of real numbers of HOL-Light and Coq

Participants: Frédéric Blanqui, Anthony Bordg, Amal Makni.

More recently, we formally proved in Coq that the types of real numbers in HOL-Light and in the Coq standard library are isomorphic, and the basic functions (addition, multiplication, etc.) and predicates (ordering) on real numbers are equal extensionally. A paper is in preparation.

7.5.7 Translating TSTP proofs to Lambdapi

Participants: Frédéric Blanqui, Guillaume Burel.

With our help, Geoff Sutcliffe extended his tool GDV for checking the correctness of TSTP proofs generated by automated theorem provers so that it now outputs Lambdapi proofs using ZenonModulo. GDV now subsumes the tool Ekstrakto developped by our former PhD student Mohamed Yacine El Haddad.

9.1.1 Inria associate team not involved in an IIL or an international program

9.2.1 Visits of international scientists

9.2.2 Visits to international teams

9.3.1 COST action 20111 EuroProofNet

Frédéric Blanqui is the chair of the COST action CA20111 EuroProofNet 2022-2025 which is a research network on proofs gathering more than 500 members from 45 different countries, with an average annual budget of 200,000 euros.

9.4.1 ICSPA

Participants: Guillaume Burel, Gilles Dowek, Catherine Dubois, Olivier Hermant, Claude Stolze.

The ANR project (2022-2025) ICSPA (Interoperable and Confident Set-based Proof Assistants) has been accepted in the context of the AAPG 2021 call. It is coordinated by Catherine Dubois and has Samovar, Inria Grand Est, Inria Paris-Saclay, LIRMM, IRIT as academic partner, and Clearsy as industrial partner. The project starts on January 1st 2022. This project aims at reinforcing the confidence in proofs carried out mechanically for the set-based specification formalisms B, Event-B, and TLA+ that are used in industry.This will be done by verifying these proofs formally and independently with the proof verifier Dedukti. The project also aims at designing and implementing an exchange framework, through which those three systems can share their proofs and theories, making them effectively interoperable.

9.4.2 PROGRAMme

Participants: Gilles Dowek.

The ANR PROGRAMme is an ANR for junior researcher Liesbeth Demol (CNRS, UMR 8163 STL, University Lille 3) to which G. Dowek participates. The subject is: “What is a program? Historical and Philosophical perspectives”. This project aims at developing the first coherent analysis and pluralistic understanding of “program” and its implications to theory and practice.

10.1.1 Scientific events: organisation

10.1.2 Scientific events: selection

10.1.3 Journal

10.1.4 Invited talks

• Théo Winterhalter was invited to give a talk at the CHoCoLa meeting in Lyon, on 21 November.
• Frédéric Blanqui was keynote speaker at the 15th International Conference on Interactive Theorem Proving (ITP'24).
• Frédéric Blanqui was invited lecturer at the 14th International School on Rewriting (ISR'24).
• Valentin Blot was an invited speaker at the Logic Colloquium 2024 (LC'24).

10.1.5 Research administration

• Frédéric Blanqui is chair of the COST action CA20111 EuroProofNet.
• Frédéric Blanqui is Vice Director of the STIC Doctoral School of the University Paris Saclay, in charge of the budget.
• Frédéric Blanqui is a member of the Scientific Committee of Inria Saclay, and Vice President since November 2024.
• Catherine Dubois is one of the two co-chairs of Groupement de Recherche Génie de la Programmation et du Logiciel (Gdr GPL).

10.2.1 Teaching

• Master: Frédéric Blanqui, formal languages, 21h, M1, ENSIIE, France
• Master: Frédéric Blanqui, rewriting theory, 14h, M1, ENS Paris-Saclay, France
• Master: Théo Winterhalter, Proof Assistants, 12h, M2, MPRI, France
• License: Luc Chabassier, Logique, L3, 30h, ENS Paris-Saclay, France
• License: Luc Chabassier, Projet base de données, 22h30, L3, ENS Paris-Saclay, France
• License: Luc Chabassier, Architecture et système, 22h30, L3, ENS Paris-Saclay, France
• License: Nicolas Margulies, Compilation project, 15h, L3, ENS Paris-Saclay, France
• License: Nicolas Margulies, Architecture et système, 22h30, L3, ENS Paris-Saclay, France
• License: Yoan Géran, Compilation project, 15h, L3, ENS Paris-Saclay, France
• License: Yoan Géran, Projet Programmation, 30h, L3, ENS Paris-Saclay, France
• IUT: Luc Chabassier, C++ R101-2, première année, 38h30, IUT d'Orsay, France
• IUT: Luc Chabassier, Projet C++ S102, première année, 10h30, IUT d'Orsay, France
• IUT: Claude Stolze, C++ R101-2, première année, 33h, IUT d'Orsay, France
• Engineering school: Thomas Traversié, Algorithmique et complexité, 18h, first year, CentraleSupélec, France
• Engineering school: Thomas Traversié, Systèmes d'information et Programmation, 22h30, first year, CentraleSupélec, France
• Engineering school: Thomas Traversié, Informatique théorique, 19h30, second year, CentraleSupélec, France
• Engineering school: Thomas Traversié, Modélisation logique et systèmes formels, 10h30, third year, CentraleSupélec, France
• Engineering school: Thomas Traversié, Modélisation logique, 7h30, third year, CentraleSupélec, France

10.2.2 Computer Science Education

• Catherine Dubois is a member of the formal methods teaching committee whose aim is to support a worldwide improvement in learning formal methods committee. In this context she co-authored an article which advocates "FM thinking", that is the application of ideas from Formal Methods applied in informal, lightweight, practical and accessible ways 15.

10.2.3 Supervision

• Théo Winterhalter co-supervises (30%) Yann Leray who is doing a PhD in the Gallinette team in Nantes.
• Frédéric Blanqui supervises the PhDs of Rishikesh Vaishnav and Melanie Taprogge.
• Catherine Dubois and Valentin Blot are supervising the PhD of Amélie Ledein.
• Catherine Dubois and Burkhart Wolff are supervising the PhD of Benoit Ballenghien.

• Théo Winterhalter supervised the M2 internship of Ewen Broudin–Caradec.
• Catherine supervised the M2 internship of Salwa Combet Gonzalez.
• Frédéric Blanqui supervised the M1 internship of Amal Makni.
• Valetin Blot supervised the M2 internship of Thomas Laure.

10.2.4 Juries

• Théo Winterhalter was an examiner and exam designer for the ENS Computer Science competitive entrance exam 2024.
• Frédéric Blanqui was a reviewer of the PhD of Thibault Hilaire (Bordeaux University).
• Catherine Dubois was a reviewer of the HDR of Frédéric Dabrowski (Université d'Orléeans)
• Catherine Dubois was a reviewer of the PhD of Benjamin Somers (IMT Atlantique).
• Catherine Dubois was a reviewer of the PhD of Olivier Martinot (Université Paris Cité).
• Catherine Dubois was a reviewer of the PhD of Mohammed El Amin Tebib (Université Grenoble Alpes).
• Catherine Dubois was an examiner of the PhD of Mariya Naumcheva (Université de Toulouse).
• Catherine Dubois was an examiner of the PhD of Camilo Correa Restrepo (Sorbonne Université).

International journals

• 13 articleC.-C.Cezar-Constantin Andrici, Ș.Ștefan Ciobâcă, C.Cătălin Hriţcu, G.Guido Martínez, E.Exequiel Rivas, É.Éric Tanter and T.Théo Winterhalter. Securing Verified IO Programs Against Unverified Code in F*.Proceedings of the ACM on Programming Languages8POPL2024, 2226-2259HALDOI
• 14 articleP.Pablo Arrighi, G.Gilles Dowek and A.Amélia Durbec. Time arrow without past hypothesis: a toy model explanation.New Journal of Physics2611November 2024, 113019HALDOI
• 15 articleB.Brijesh Dongol, C.Catherine Dubois, S.Stefan Hallerstede, E.Eric Hehner, C.Carroll Morgan, P.Peter Müller, L.Leila Ribeiro, A.Alexandra Silva, G.Graeme Smith and E.Erik de Vink. On formal methods thinking in computer science education.Formal Aspects of Computing371December 2024, 1-23HALDOIback to text
• 16 articleT.Thiago Felicissimo and F.Frédéric Blanqui. Sharing proofs with predicative theories through universe-polymorphic elaboration.Logical Methods in Computer ScienceSeptember 2024HAL
• 17 articleM.Matthieu Sozeau, Y.Yannick Forster, M.Meven Lennon-Bertrand, J. B.Jakob Botsch Nielsen, N.Nicolas Tabareau and T.Théo Winterhalter. Correct and Complete Type Checking and Certified Erasure for Coq, in Coq.Journal of the ACM (JACM)November 2024, 1-76HALDOI
• 18 articleT.Théo Winterhalter. Dependent Ghosts Have a Reflection for Free.Proceedings of the ACM on Programming Languages258August 2024, 630-658HALDOIback to text

International peer-reviewed conferences

• 19 inproceedingsP.Pablo Arrighi, G.Gilles Dowek and A.Amélia Durbec. A toy model provably featuring an arrow of time without past hypothesis.LNCSRC 2024 - 16th International Conference on Reversible Computation14680Lecture Notes in Computer ScienceTorun, PolandSpringer Nature SwitzerlandMay 2024, 50-68HALDOI
• 20 inproceedingsF.Frédéric Blanqui. Translating HOL-Light proofs to Coq.Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and ReasoningLPAR-25 - 25th International Conference on Logic for Programming, Artificial Intelligence and ReasoningBalaclava, MauritiusMay 2024, 1--18HALDOIback to text
• 21 inproceedingsV.Valentin Blot, G.Gilles Dowek, T.Thomas Traversié and T.Théo Winterhalter. From Rewrite Rules to Axioms in the λΠ-Calculus Modulo Theory.Lecture Notes in Computer Science, International Conference on Foundations of Software Science and Computation StructuresFoSSaCS 2024 - 27th International Conference on Foundations of Software Science and Computation Structures14575Lecture Notes in Computer Science2Luxembourg City, LuxembourgSpringer Nature SwitzerlandApril 2024, 3-23HALDOIback to text
• 22 inproceedingsA.Alessio Coltellacci, G.Gilles Dowek and S.Stephan Merz. Reconstruction of SMT proofs with Lambdapi.CEUR Workshop ProceedingsSMT 2024 - 22nd International Workshop on Satisfiability Modulo Theories3725Montréal, CanadaJuly 2024, 13-23HAL
• 23 inproceedingsC.Catherine Dubois. Deductive Verification of Sparse Sets in Why3.Verified Software. Theories, Tools and Experiments - 16th International Conference, VSTTE 2024, PostproceedingsVSTTE 2024 - 16th International Conference on Verified Software: Theories, Tools, and ExperimentsPrague, Czech RepublicOctober 2024HALback to text
• 24 inproceedingsT.Thiago Felicissimo. Generic bidirectional typing for dependent type theories.ESOP 2024 - 33rd European Symposium on ProgrammingLuxembourg City, LuxembourgApril 2024HALback to text
• 25 inproceedingsT.Thiago Felicissimo. Second-order Church-Rosser modulo, without normalization.Proceedings of the 13th International Workshop on Confluence - IWC 2024IWC 2024 – 13th International Workshop on ConfluenceTallinn, EstoniaJuly 2024HALback to text
• 26 inproceedingsT.Thiago Felicissimo and T.Théo Winterhalter. Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti.9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)Formal Structures for Computation and DeductionTalinn, Estonia2024HALback to text
• 27 inproceedingsP. G.Philipp G Haselwarter, B. S.Benjamin Salling Hvass, L. L.Lasse Letager Hansen, T.Théo Winterhalter, C.Cătălin Hriţcu and B.Bas Spitters. The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography.CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and ProofsCPP 2024 - 13th ACM SIGPLAN International Conference on Certified Programs and ProofsLondon, United KingdomACMJanuary 2024, 30-44HALDOI
• 28 inproceedingsY.Yann Leray, G.Gaëtan Gilbert, N.Nicolas Tabareau and T.Théo Winterhalter. The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant.International Conference on Interactive Theorem Proving (ITP 2024)15th International Conference on Interactive Theorem Proving (ITP 2024)Tbilisi, GeorgiaSeptember 2024, 18HALDOIback to text
• 29 inproceedingsT.Thomas Traversié. Kuroda's Translation for the λΠ-Calculus Modulo Theory and Dedukti.Electronic Proceedings in Theoretical Computer ScienceLFMTP 2024 - International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice404Tallinn, EstoniaJuly 2024, 35-48HALDOIback to text
• 30 inproceedingsT.Thomas Traversié. Proofs for Free in the λΠ-Calculus Modulo Theory.Electronic Proceedings in Theoretical Computer ScienceLFMTP 2024 - International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice404Tallinn, EstoniaJuly 2024, 49 - 63HALDOIback to text

National peer-reviewed Conferences

• 31 inproceedingsM.Maximiliano Cristiá and C.Catherine Dubois. Comparing EventB, {log} and Why3 Models of Sparse Sets.JFLA 2024 - 35es Journées Francophones des Langages ApplicatifsSaint-Jacut-de-la-Mer, FranceJanuary 2024HALback to text

Doctoral dissertations and habilitation theses

• 32 thesisL.Louise Dubois de Prisque. Compositional preprocessing in Coq.Université Paris-SaclayJuly 2024HALback to text
• 33 thesisT.Thiago Felicissimo. Generic bidirectional typing in a logical framework for dependent type theories.Université Paris-SaclaySeptember 2024HALback to text

Reports & preprints

• 34 miscG.Gilles Dowek. La dynamique des noms propres.2024HAL
• 35 miscC.Claude Stolze, O.Olivier Hermant and R.Romain Guillaumé. Towards Formalization and Sharing of Atelier B Proofs with Dedukti.January 2024HALback to text
• 36 miscT.Thomas Traversié. Kuroda's Translation for Higher-Order Logic.April 2024HALback to text
• 37 miscR.Rishikesh Vaishnav. A Term-Patching Framework for Eliminating Definitional Equalities in Lean (Work-in-Progress).December 2024HALback to text

Other scientific publications

• 38 thesisM.Melanie Taprogge. Computer-Assisted Proof Verification for Higher-Order Automated Reasoning within the Dedukti Framework: A Thesis submitted for the Degree of Master of Science.Universität GreifswaldGreifswaldJuly 2024, 96HALback to text