2025Activity report​​Project-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
• Publications:
  hal-02981561,‌ hal-05237915
• 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://­github.­com/­Deducteam/­Dedukti
• Publications:
  hal-01086609,‌​‌ hal-01176715, hal-01441751,​​ tel-01299180
• Contact:
  Frederic Blanqui​​​‌

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
• Publication:
  hal-04613926​​​‌
• Contact:
  Frederic Blanqui

6.1.4​ 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
• Publication:
  tel-05229403​‌
• Contact:
  Luc Chabassier

6.1.5​​ 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
• Publication:​‌
  hal-00909784
• Contact:
  Guillaume Burel​​
• Partner:
  ENSIIE

6.1.6 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:
  Bruno​​ Barras

6.1.7 TranslationTemplates

• Keyword:​​​‌
  Dedukti
• Functional Description:
  The​ tool offers three types​‌ of translations (theory morphisms,​​ logical relations, theory embeddings)​​​‌ to be instantiated with​ user-specified parameters, in order​‌ to translate proofs between​​ two theories encoded in​​​‌ Dedukti.
• Publication:
  hal-05027872
• Contact:​
  Thomas Traversie

7.1.1​​​‌ Lambdapi

Participants: Frédéric Blanqui​, Bruno Barras,​‌ Claudio Sacerdoti Coren,​​ Abdelghani Alidra.

The​​​‌ proof assistant Lambdapi has​ been improved on various​‌ aspects and a new​​ release has been done​​​‌ in July 2025. The​ Bindlib library for representing​‌ binders has been replaced​​ by the use of​​​‌ de Bruijn indices. The​ efficiency of reduction and​‌ conversion has been improved​​ a lot. New commands​​​‌ have been added to​ index symbols and rules,​‌ make queries against this​​ index, and run a​​​‌ web server to make​ queries online. New proof​‌ tactics have been added​​ including a tactic that​​​‌ can turn a term​ into a tactic, hence​‌ providing a way to​​ define tactics using rewriting.​​​‌ The Menhir parser has​ been replaced by a​‌ new LL(1) parser written​​ by hand with equal​​​‌ efficiency but better error​ messages.

7.1.2 Indexing and​‌ search of proof libraries​​

Participants: Abdelghani Alidra,​​​‌ Claudio Sacerdoti Coen.​

Dedukti and MMT are​‌ both examples of tools​​ that can collect mathematical​​​‌ libraries coming from different​ systems in a unified​‌ but heterogeneous body. Indeed,​​ both tools implement a​​​‌ logical framework where the​ logics or type systems​‌ of the various mathematical​​ assistants can be represented,​​​‌ so that their libraries​ can be encoded in​‌ a single format preserving​​ well-typedness. Still, the images​​​‌ of the various libraries​ remain disjoint: logical consistency​‌ of their union is​​ not granted, the encoding​​ of the various statements​​​‌ differs from logic to‌ logic, and the same‌​‌ mathematical entity remains defined​​ repeatedly and independently. To​​​‌ benefit from the common‌ representation, then, additional tools‌​‌ need to be developed,​​ for example, to translate​​​‌ results encoded in the‌ representation of a logic‌​‌ into the representation of​​ a stronger logic, taking​​​‌ care of aligning the‌ duplicated mathematical entities. In‌​‌ 17, we addressed​​ the challenges posed by​​​‌ indexing and searching large‌ heterogeneous libraries. For example,‌​‌ users may expect to​​ find results in the​​​‌ library up to the‌ encoding used and up‌​‌ to alignments, so to​​ be able to mix​​​‌ in the search result‌ statements originally coming from‌​‌ different systems and logics.​​ In particular, we describe​​​‌ new indexing and retrieval‌ capabilities that we integrated‌​‌ directly into the Lambdapi​​ proof assistant, that can​​​‌ work on Dedukti files.‌ Moreover, we set up‌​‌ a web server on​​ lambdapi.saclay.inria.fr where users can​​​‌ input queries on the‌ coq-hol-light library, which contains‌​‌ a translation of the​​ HOL-Light Multivariate library. This​​​‌ was presented at the‌ RocqPL'26 workshop 16.‌​‌

7.1.3 A logical framework​​ for dealing with languages​​​‌ with binders, automatically and‌ fast

Participants: Mathis Bouverot-Dupuis‌​‌, Théo Winterhalter.​​

When studying a programming​​​‌ language or type system‌ in a proof assistant‌​‌ such as Rocq, one​​ often has to deal​​​‌ with the notion of‌ binders, variable representation and‌​‌ then substitution. Something which​​ is usually a tedious​​​‌ and repetitive task. Tools‌ such as Autosubst  37‌​‌, 38 have been​​ quite successful at alleviating​​​‌ this burden by generating‌ boilerplate code automatically from‌​‌ a succinct description of​​ the language's syntax. It​​​‌ also comes with a‌ very handy tactic for‌​‌ simplifying expressions containing substitutions.​​ However, this tactic is​​​‌ extremely slow. We thus‌ worked on providing a‌​‌ tool similar to Autosubst,​​ which we called Sulfur​​​‌ (Substitution l‌ogical framework u‌​‌sing reflection) a​​ Rocq plugin that attempts​​​‌ to solve the performance‌ issues of Autosubst by‌​‌ implementing the simplification tactic​​ as a reflective tactic​​​‌  30.

This work‌ led to a talk‌​‌ given at the RocqPL​​ workshop of POPL 2026,​​​‌ joint work with Kathrin‌ Stark and Kenji Maillard‌​‌  31.

7.2.1 Sort polymorphism‌ in type theory

Participants:‌​‌ Théo Winterhalter, Johann​​ Rosain.

Universes, or​​​‌ sorts, are essentially the‌ types of types, initially‌​‌ split between Prop for​​ propositions, and Type for​​​‌ regular data types. Recently,‌ a new sort SProp‌​‌ was added to Rocq,​​ and we proposed to​​​‌ add yet another, called‌ Ghost to represent ghost‌​‌ data  39. Increasing​​ the number of sorts​​​‌ means dupplication for constructions‌ that involve them: for‌​‌ instance the product of​​ types $A\times \mathrm{B‌}$ and conjunction of propositions‌ $P\wedge Q$ are‌​‌ morally the same and​​ could in principle be​​​‌ factored into a single‌ definition. To this end‌​‌ we introduced the notion​​ of bounded sort polymorphism,​​​‌ which has been implemented‌ in Rocq by Johann‌​‌ Rosain during his internship​​​‌ with Théo Winterhalter in​ Deducteam and Matthieu Sozeau​‌ in Gallinette (Inria Rennes).​​

This work led to​​​‌ a publication at POPL​ 2026 15.

7.2.2​‌ Controlling computation in type​​ theory

Participants: Théo Winterhalter​​​‌, Yann Leray.​

Proof assistants rely on​‌ computation to identify expressions​​ such as $3+‌2$ and 5 without​ any user input, thus​‌ providing a user experience​​ closer to what one​​​‌ does on paper. In​ order to give users​‌ more control over computation,​​ we worked on extending​​​‌ proof assistants—and in particular​ Rocq—with user-defined computation rules​‌ (or rewrite rules). Beyond​​ the implementation, we studied​​​‌ the meta-theory of such​ an extension, establishing constraints​‌ under which the expected​​ properties of the systems​​​‌ are not broken. For​ instance, as proof assistants​‌ are used to check​​ proofs, it is important​​​‌ that our additions do​ not break the proof​‌ checking algorithm, which happens​​ if we do not​​​‌ impose restrictions. We went​ further and studied the​‌ possibility of having such​​ rules be only local​​​‌ to a certain context,​ giving the possibility to​‌ instantiate them later. With​​ this, we show that​​​‌ certain features of proof​ assistants can safely be​‌ assumed just by virtue​​ of them having an​​​‌ encoding, without increasing the​ trusted code base or​‌ having to use the​​ encoding explicitly.

The work​​​‌ on global rewrite rules​ in Rocq has been​‌ submitted 26 as an​​ extended version of the​​​‌ ITP paper from last​ year  35. The​‌ work on local rewrite​​ rules has been accepted​​​‌ at POPL 2026 14​ and received a distinguished​‌ paper award.

7.2.3 Confluence​​ of higher-order rewriting

Participants:​​​‌ Jean-Pierre Jouannaud.

Powerful​ confluence criteria for higher-order​‌ rewriting exist for left-linear​​ systems, even in the​​​‌ presence of critical pairs​ and non-termination. On the​‌ other hand, confluence criteria​​ that allow for mixing​​​‌ non-termination and non-left-linearity are​ either extremely limited or​‌ hardly usable in practice.​​ In 25, together​​​‌ with Thiago Felicissimo, a​ former PhD student of​‌ Deducteam now in postdoc​​ in Gallinette, we study​​​‌ confluence criteria which explore​ sort information to make​‌ proving higher-order confluence possible,​​ even in the presence​​​‌ of non-termination and non-left-linearity.​ We give many interesting​‌ examples of systems covered​​ by our results, including​​​‌ a calculus issuing from​ a dependent type theory​‌ with cumulative universes.

7.2.4​​ DRAG rewriting

Participants: Jean-Pierre​​​‌ Jouannaud.

Together with​ Nachum Dershowitz and Fernando​‌ Orejas, we present in​​ 32 a new and​​​‌ powerful algebraic framework for​ graph rewriting, based on​‌ drags, a class of​​ directed graphs whose vertices​​​‌ are labeled with function​ symbols that govern the​‌ number of their outgoing​​ edges. Some vertices without​​​‌ successors are labeled by​ variables, making terms and​‌ dags particular cases of​​ drags. Vertices are embellished​​​‌ with roots. Roots and​ sprouts can be wired​‌ together to form edges,​​ giving rise to a​​​‌ novel composition operator. Drag​ rewriting naturally extends graph​‌ rewriting, dag rewriting, and​​ term rewriting models. This​​​‌ work is submitted to​ be part of a​‌ book.

7.3.1​​ Expressing Lean definitions and​​​‌ proofs in Dedukti

Participants:‌ Rishikesh Vaishnav.

During‌​‌ the past year, work​​ was done to integrate​​​‌ the "Lean4Less" translation within‌ Lean2dk (the tool for‌​‌ translating proofs from Lean​​ to Dedukti). Lean4Less is​​​‌ used by Lean2dk as‌ a "pre-translation" step that‌​‌ first translates Lean terms​​ into a form that​​​‌ can be checked by‌ a smaller kernel, which‌​‌ we call "Lean-". The​​ rules used by Lean-​​​‌ are a subset of‌ the rules of Lean‌​‌ which are amenable to​​ a direct encoding within​​​‌ Dedukti. Given input terms‌ typable in Lean-, Lean2dk‌​‌ is then able to​​ translate these to Dedukti​​​‌ without having to consider‌ particular definitional equalities, notably‌​‌ those of proof irrelevance​​ and "K-like reduction". Overall,​​​‌ this full translation pipeline‌ has shown some promising‌​‌ first results in its​​ ability to translate significant​​​‌ subsets of the Lean‌ standard library to Dedukti.‌​‌ However, the translation ran​​ into issue with scaling​​​‌ which we suspect are‌ attributable redundancie in the‌​‌ output Dedukti representation, where​​ common subterms are duplicated​​​‌ in the output rather‌ than shared (as they‌​‌ would be in the​​ ".olean" files they originate​​​‌ from). We have begun‌ some work to make‌​‌ explicit the sharing of​​ certain categories of subterms​​​‌ (in particular the translation‌ of Lean's universe level‌​‌ expressions) through the use​​ of auxiliary defined functions.​​​‌ However, more work remains‌ to be done to‌​‌ further expand this subterm​​ sharing, and investigate other​​​‌ possible ways to enable‌ more efficient scaling.

7.3.2‌​‌ Making Leo-III output Lambdapi​​ proofs

Participants: Melanie Taprogge​​​‌.

Over the past‌ year, substantial progress has‌​‌ been made on the​​ translation of proofs produced​​​‌ by the higher-order logic‌ automated theorem prover Leo-III‌​‌ to Lambdapi. The verification​​ of these proofs requires​​​‌ both the encoding of‌ the underlying rules of‌​‌ the calculus EP in​​ Lambdapi, and the automated​​​‌ generation of proof steps,‌ including the handling of‌​‌ edge cases. Support for​​ multiple additional inference rules​​​‌ was implemented, raising the‌ current version's coverage of‌​‌ verifiable proofs from the​​ TPTP library—the community standard​​​‌ benchmark—to nearly 80%. This‌ progress includes partial verification‌​‌ of processes known to​​ be particularly challenging for​​​‌ automated reasoning systems, most‌ notably clausification and, in‌​‌ particular, Skolemisation. During this​​ process, several bugs in​​​‌ Leo-III were identified and‌ subsequently fixed. In parallel,‌​‌ work was initiated on​​ the integration of Leo-III​​​‌ into the tool GDV,‌ with the long-term objective‌​‌ of enabling the independent​​ verification of proof traces​​​‌ in the TSTP format‌ produced by automated theorem‌​‌ provers. GDV is currently​​ limited to first-order logic,​​​‌ this work lays important‌ groundwork for its extension‌​‌ to higher-order verification. Beyond​​ direct support for Leo-III,​​​‌ this work also contributes‌ more broadly to the‌​‌ Lambdapi and proof verification​​ communities. A systematic and​​​‌ generally applicable framework for‌ encoding proof steps of‌​‌ automated proof systems has​​ been developed, with a​​​‌ focus on reusability across‌ different systems. As part‌​‌ of this effort, several​​ reusable encodings of commonly​​​‌ used inference rules were‌ added to the Lambdapi‌​‌ standard library. Finally, a​​​‌ dedicated library containing the​ Leo-III encodings was published,​‌ the encoded rules of​​ the EP calculus are​​​‌ modular and can be​ reused in other contexts​‌ where applicable. A publication​​ describing the progress of​​​‌ the project to date​ is currently under preparation.​‌

7.4.1 From extensional​ to intensional type theory​‌ in Lean

Participants: Rishikesh​​ Vaishnav.

In 2025,​​​‌ we completed the development​ of the tool "Lean4Less"​‌ for translating Lean proofs​​ to be checkable in​​​‌ a smaller theory, which​ we call "Lean-", lacking​‌ in particular Lean's definitional​​ equalities of proof irrelevance​​​‌ and "K-like reduction". The​ goal of translating to​‌ this smaller theory is​​ to ease the later​​​‌ translation of these Lean-​ proofs into Dedukti. The​‌ translation is based on​​ a general translation from​​​‌ extensional to intensional type​ theory, which we have​‌ adapted to Lean, interpreting​​ Lean as an "extensional"​​​‌ version of Lean- where​ extensionality is limited to​‌ a single propositional equality​​ representing proof irrelevance. Our​​​‌ implementation has proven successful​ in translating medium-sized libraries​‌ (for instance the Lean​​ standard library and some​​​‌ lower-level mathlib modules) to​ the Lean- theory, and​‌ has seen significant interest​​ from the larger Lean​​​‌ community in the potential​ to adapt it for​‌ various purposes (e.g. in​​ defining a translation from​​​‌ a hypothetical extensional version​ of Lean). This work​‌ was published in the​​ proceedings of ICTAC'25 20​​​‌.

7.4.2 Translations between​ classical, intuitionistic and minimal​‌ logics

Participants: Thomas Traversié​​, Olivier Hermant.​​​‌

Classical logic can be​ embedded into intuitionistic logic​‌ by inserting double negations​​ inside formulas, such that​​​‌ a formula and its​ translation are equivalent in​‌ classical logic. Recently, Brown​​ and Rizkallah extended Kuroda's​​​‌ 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 the classical equivalence​​ does not generally hold​​​‌ in higher-order logic, and​ that it does under​‌ functional extensionality and propositional​​ extensionality. Moreover, we emphasized​​​‌ a condition under which​ Kuroda’s translation works with​‌ functional extensionality. This work​​ has been submitted for​​​‌ publication 27.

Several​ translations generalize double-negation translations​‌ by using monad operators​​ instead of double negations.​​​‌ They eliminate particular axioms,​ for instance the principle​‌ of excluded middle or​​ the principle of explosion,​​​‌ and therefore can be​ used to embed classical​‌ logic into intuitionistic logic​​ or intuitionistic logic into​​​‌ minimal logic. Such translations​ have been defined for​‌ first-order logic. We defined​​ a translation, parameterized by​​​‌ monad operators, for higher-order​ logic. In particular, the​‌ property that any formula​​ and its translation are​​​‌ equivalent in the presence​ of the eliminated axiom​‌ holds under functional extensionality​​ and propositional extensionality. We​​​‌ applied this translation to​ embed higher-order classical (respectively​‌ intuitionistic) logic into higher-order​​ intuitionistic (respectively minimal) logic.​​​‌ We identified a constructive​ fragment of higher-order classical​‌ logic. This work has​​ been published in 19​​​‌.

7.4.3 Translating HOL-Light​ proofs to Dedukti, Lambdapi​‌ and Rocq

Participants: Frédéric​​ Blanqui.

The software​​ hol2dk has been improved​​​‌ further, and the whole‌ HOL-Light Multivariate library (about‌​‌ 17,500 theorems on real​​ and complex analysis) has​​​‌ been automatically translated to‌ Lambdapi, and then‌​‌ to Rocq thanks to​​ the export to Rocq​​​‌ functionality available in Lambdapi.‌ In this translation, the‌​‌ basic HOL-Light types and​​ functions on natural numbers,​​​‌ real numbers and integers‌ are substituted by those‌​‌ of the Rocq standard​​ library, making the theorems​​​‌ obtained by translation directly‌ usable by Rocq users.‌​‌

7.4.4 Alignment of HOL-Light​​ and Rocq libraries

Participants:​​​‌ Frédéric Blanqui, Antoine‌ Gontard.

We proved‌​‌ that the type definitions​​ of real numbers in​​​‌ HOL-Light and Rocq are‌ isomorphic, as well as,‌​‌ the types of integers.​​ We also proved that​​​‌ several basic functions on‌ those types have equivalent‌​‌ definitions in HOL-Light and​​ Rocq. Hence, when translating​​​‌ HOL-Light to Rocq, we‌ can now substitute HOL-Light‌​‌ types or functions by​​ those of the Rocq​​​‌ standard library. This way,‌ a HOL-Light theorem on‌​‌ HOL-Light real numbers can​​ be translated into a​​​‌ Rocq theorem on Rocq‌ real numbers, and thus‌​‌ can be directly applied​​ in other Rocq developments.​​​‌ We did this with‌ the HOL-Light Multivariate library‌​‌ which contains thousands of​​ theorems on real and​​​‌ complex analysis. The resulting‌ Rocq library is available‌​‌ as the Opam package​​ coq-hol-light.

During his​​​‌ internship, Antoine Gontard developed‌ Rocq tactics for automatically‌​‌ proving that a HOL-Light​​ definition of an inductive​​​‌ type is isomorphic to‌ the corresponding Rocq definition,‌​‌ and that a recursive​​ function definition in HOL-Light​​​‌ is equal to its‌ corresponding Rocq definition. Note‌​‌ that, in Rocq, inductive​​ types are primitive while,​​​‌ in HOL-Light, they are‌ defined as some subset‌​‌ of some complex tree​​ structure. In Rocq, functions​​​‌ are defined by using‌ pattern-matching while, in HOL-Light,‌​‌ they are defined by​​ using a choice operator​​​‌ and equations.

Thanks to‌ those tactics, Antoine could‌​‌ automatically translate the HOL-Light​​ Logic library to Rocq​​​‌ and substitute HOL-Light type‌ and function definitions by‌​‌ Rocq idiomatic definitions. The​​ resulting Rocq library is​​​‌ now available as the‌ Opam package rocq-hollight-logic.‌​‌ It contains many useful​​ theorems on the first-order​​​‌ logic: upward Löwenheim-Skolem, downward‌ Löwenheim-Skolem, compactness theorem, Skolem-Gödel-Herbrand‌​‌ theorem, Herbrand theorem, completeness​​ of resolution, Birkhoff's theorem,​​​‌ well-foundedness of the lexicographic‌ path ordering, etc.

7.4.5‌​‌ Translating TSTP proofs to​​ Lambdapi

Participants: Frédéric Blanqui​​​‌, Guillaume Burel,‌ Geoff Sutcliffe.

We‌​‌ made Geoff Sutcliffe's GDV​​ tool for checking the​​​‌ correctness of TSTP proofs‌ exported by automated theorem‌​‌ provers output Lambdapi proofs​​ for CNF problems by​​​‌ using ZenonModulo. The‌ corresponding workflow, which aims‌​‌ at increasing our trust​​ in the results of​​​‌ automated theorem provers, is‌ explained in detail in‌​‌ 18.

7.4.6 Translation​​ templates between Dedukti theories​​​‌

Participants: Thomas Traversié.‌

Since the $\lambda \mathrm{\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 $\mathrm{\lambda ‌}\Pi$-calculus modulo rewriting.‌​‌ Several translations templates already​​​‌ exist for LF, for​ instance theory morphisms  34​‌ and logical relations  36​​, 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 \mathrm{\Pi ‌}$-calculus modulo rewriting. We​​ implemented TranslationTemplates, that​​​‌ applies these translation templates​ to Dedukti, and we​‌ formalized different case studies.​​ This work is the​​​‌ result of a collaboration​ with Florian Rabe (University​‌ of Erlangen) and was​​ submitted for publication 28​​​‌.

7.4.7 Translating Eunoia​ logics and proofs to​‌ Lambdapi

Participants: Ciarán Dunne​​, Guillaume Burel.​​​‌

We have developed a​ tool, eo2lp, for​‌ translating signatures and proof​​ scripts from the logical​​​‌ framework Eunoia to the​ Lambdapi proof assistant. The​‌ SMT solver cvc5 uses​​ Eunoia as the default​​​‌ output format for proof​ production, and the rules​‌ used by these proofs​​ are formalized as the​​​‌ Eunoia signature cpc.​

We overcame some previous​‌ roadblocks to this work​​ whilst visiting Haniel Barbosa​​​‌ at UFMG, Belo-Horizonte, in​ a trip funded by​‌ the Inria associated term​​ project CARMA. In particular,​​​‌ we altered our elaboration​ and encoding mechanism to​‌ better accomodate Eunoia's idiosyncratic​​ handling of application, elaboration​​​‌ and overloading. This advancement​ has allowed us to​‌ translate a larger portion​​ of cpc in Lambdapi,​​​‌ and therefore import a​ larger number of proof​‌ certificates generated by cvc5​​ .

A paper 24​​​‌ is in preparation and​ will be submitted soon.​‌

7.4.8 Translating Predicate Prover​​ traces to Lambdapi

Participants:​​​‌ Ciarán Dunne, Catherine​ Dubois, Guillaume Burel​‌.

The Predicate Prover​​ (PP) is a first-order​​​‌ automated theorem prover used​ as by Atelier B,​‌ whose results are trusted​​ as an oracle. To​​​‌ increase confidence in these​ results, we have developed​‌ pp2lp, a tool​​ to translate proof traces​​​‌ from PP into independently​ verifiable Lambdapi proof scripts.​‌ We began by formalizing​​ the proof system of​​​‌ PP in Lambdapi. Next,​ we built our OCaml​‌ tool to parse proof​​ traces (each consists of​​​‌ a sequence of rule​ applications), and reconstructs a​‌ forward-style proof in Lambdapi's​​ syntax. This work enables​​​‌ the formal verification of​ proofs generated by a​‌ closed-source, industrial theorem prover​​ within the Lambdapi ecosystem.​​​‌

The project is supported​ by the ICSPA ANR​‌ project and will continue​​ until June 2026.

7.5.1 Secure​ interoperability between stateful verified​‌ and unverified code in​​ F*

Participants: Théo Winterhalter​​​‌.

We worked towards​ the goal of secure​‌ interoperability between verified higher-order​​ effectful code (typically generated​​​‌ in a proof assistant)​ and unverified code (written​‌ in a regular programming​​ language such as OCaml).​​​‌ To that end, we​ introduced SecRef*, a secure​‌ compilation framework protecting stateful​​ programs verified in F*​​​‌ against linked unverified code,​ with which the program​‌ dynamically shares ML-style mutable​​ references. This work was​​​‌ published at ICFP 2025​ 13.

7.5.2 Deductive​‌ Verification of programs

Participants:​​ Catherine Dubois.

We​​​‌ have continued our work​ on the formal verification​‌ of data structures used​​ to represent variable domains​​ in constraint solvers. Using​​​‌ the Why3 platform, we‌ have developed a formally‌​‌ verified implementation of set​​ domains based on sparse​​​‌ sets. This new contribution‌ has been published in‌​‌ JFPC 2025 21.​​

7.5.3 Runtime Verification of​​​‌ Inductive Predicates

Participants: Catherine‌ Dubois.

The logical‌​‌ annotations language ACSL (ANSI/ISO​​ C specification Language) includes​​​‌ inductively defined predicates. In‌ collaboration with Julien Signoles‌​‌ and Jan Rochel (CEA​​ List), we are working​​​‌ on the runtime verification‌ of such predicates. We‌​‌ propose a three-valued semantics​​ of E-ACSL inductive predicates​​​‌ and a semantics-preserving translation‌ of a subset of‌​‌ such predicates into an​​ easy-to-execute form. An implementation​​​‌ of this translation has‌ been added to the‌​‌ E-ACSL plug-in of Frama-C.​​

8.1.1‌ Inria associate team not‌​‌ involved in an IIL​​ or an international program​​​‌

• We are leading the‌ associated team ICI 2024-2026‌​‌ with AIST Tokyo, Japan,​​ which aims at making​​​‌ the proof assistants Isabelle‌ and Rocq, interoperable, by‌​‌ first translating Isabelle and​​ Rocq libraries to Dedukti,​​​‌ and then the obtained‌ Dedukti libraries to Isabelle‌​‌ and Rocq, possibly after​​ some transformations.
• We also​​​‌ participate to the associated‌ team CARMA with Inria‌​‌ Nancy and Brazil, which​​ aims at improving the​​​‌ state of the art‌ in SMT solving.

8.2.1​​ Visits of international scientists​​​‌

8.2.2 Visits to international​​ teams

8.2.3 Other european‌​‌ programs/initiatives

Frédéric Blanqui is​​ the chair of the​​​‌ COST action CA20111 EuroProofNet‌ 2021-2025, which gathers more‌​‌ than 600 researchers from​​ 47 different countries, including​​​‌ all the members of‌ Deducteam. The aim of‌​‌ EuroProofNet is to boost​​ the interoperability and usability​​​‌ of proof assistants.

8.3.1 ICSPA‌​‌

Participants: Frédéric Blanqui,​​ Guillaume Burel, Gilles​​​‌ Dowek, Catherine Dubois‌, Ciarán Dunne,‌​‌ Olivier Hermant, Melanie​​ Taprogge.

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.

8.3.2 PROGRAMme​​

Participants: Gilles Dowek.​​​‌

The ANR PROGRAMme is​ an ANR for junior​‌ researchers headed by Liesbeth​​ De Mol (CNRS UMR​​​‌ 8163 STL, University Lille​ 3) to which Gilles​‌ 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.

9.1.1 Scientific events: organisation​

• Frédéric Blanqui organized the​‌ EuroProofNet Symposium in Orsay,​​ France, on 8-19 September​​​‌ 2025, which gathered about​ 150 participants over 2​‌ weeks. The symposium consisted​​ of several events:
  • The​​​‌ 1st international school on​ Logical Frameworks and Proof​‌ Systems Interoperability (FMPSI).
  • A​​ workshop on automated reasoning​​​‌ and proof logging.
  • The​ 2nd International Workshop on​‌ Highlights in Organizing and​​ Optimizing Proof-logging Systems (WHOOPS​​​‌ '25).
  • The 4th workshop​ on proof libraries.
  • The​‌ International Conference on Mathematical​​ and Computational Linguistics for​​​‌ Proofs (MCLP).
  • A workshop​ on program verification.

9.1.2 Leadership within‌​‌ the scientific community

• Frédéric​​ Blanqui is chair of​​​‌ the COST action CA20111‌ EuroProofNet 2021-2025 which gathers‌​‌ more than 600 researchers​​ from 47 different countries,​​​‌ which aims at boosting‌ the interoperability and usability‌​‌ of proof systems.

9.1.3​​ Research administration

• Frédéric Blanqui​​​‌ is chair of the‌ COST action CA20111 EuroProofNet‌​‌ 2021-2025 which gathers more​​ than 600 researchers from​​​‌ 47 different countries. EuroProofNet‌ has a yearly budget‌​‌ of about 200,000 euros.​​ Every year, it organizes​​​‌ several meetings, schools and‌ conferences, and funds short-term‌​‌ scientific missions and travel​​ grants to conference for​​​‌ your researchers from European‌ inclusive target countries.
• Frédéric‌​‌ Blanqui is deputy director​​ of the doctoral school​​​‌ in computer science STIC‌ of the University Paris‌​‌ Saclay.
• Frédéric Blanqui is​​ vice president of the​​​‌ scientific committee of Inria‌ Saclay.
• Catherine Dubois is‌​‌ one of the two​​ co-chairs of Groupement de​​​‌ Recherche Génie de la‌ Programmation et du Logiciel‌​‌ (Gdr GPL).

9.2.1 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. This committee is‌ currently working on the‌​‌ proposition on a curriculum​​ involving formal methods topics.​​​‌

9.2.2 Teaching

• Frédéric Blanqui‌ gives a 12 hours‌​‌ M1 course on rewriting​​ theory at the ENS​​​‌ Paris Saclay.
• Frédéric Blanqui‌ gives a 21 hours‌​‌ M1 course on formal​​ grammars and automata at​​​‌ the ENSIIE engineering school.‌
• Frédéric Blanqui gave a‌​‌ 6 hours lecture on​​ the $\lambda \Pi$-calculus​​​‌ modulo rewriting at the‌ 1st international school on‌​‌ logical frameworks and proof​​ systems interoperability.
• Thomas Traversié​​​‌ gave 15h75 of TD/TP‌ for the M1 course‌​‌ on theoretical computer science​​ at CentraleSupélec
• Thomas Traversié​​​‌ gave a 24 hours‌ M2 course (lectures and‌​‌ TD) on logic, formal​​ grammars and automata at​​​‌ CentraleSupélec
• Thomas Traversié supervised‌ 48 hours of the‌​‌ L1 coding project at​​ CentraleSupélec
• Antoine Gontard gave​​​‌ 12 hours of TD‌ for the M1 MPRI‌​‌ rewriting theory course at​​ the ENS Paris Saclay​​​‌
• Nicolas Margulies gave 15‌ hours of TP for‌​‌ the second L3 programmation​​ project at the ENS​​​‌ Paris-Saclay
• Nicolas Margulies gave‌ 15 hours of TP‌​‌ fot the L3 logics​​ project at the ENS​​​‌ Paris-Saclay
• Nicolas Margulies gave‌ 19h30 of TP for‌​‌ the L3 advanced web​​ programming course at the​​​‌ IUT d'Orsay
• Théo Winterhalter‌ is in charge of‌​‌ a 24-hour M2 course​​ for the MPRI, on​​​‌ the topic of Proof‌ Assistants. He teaches 12‌​‌ hours of the course.​​​‌ He is also part​ of the “comission des​‌ études”, the committee in​​ charge of the curriculum​​​‌ of the master and​ of handling the students​‌ in general, including grading​​ internship reports and defences.​​​‌

9.2.3 Supervision

• Frédéric Blanqui​ supervised the internship of​‌ Antoine Gontard.
• Théo Winterhalter​​ supervised the internship of​​​‌ Mathis Bouverot-Dupuis, and co-supervised​ with Matthieu Sozeau the​‌ internship of Johann Rosain​​ who was located in​​​‌ Nantes.
• Frédéric Blanqui is​ the thesis director of​‌ Rishikesh Vaishnav, Melanie Taprogge,​​ Antoine Gontard, Ivan Martinez​​​‌ Comas, Ewen Broudin-Caradec and​ Nicolas Margulies.
• Frédéric Blanqui​‌ supervises the PhD work​​ of Rishikesh Vaishnav, Antoine​​​‌ Gontard, Melanie Taprogge (with​ Alexender Steen), and Ivan​‌ Martinez Comas (with Patrick​​ Massot).
• Bruno Barras supervises​​​‌ the PhD work of​ Nicolas Margulies.
• Théo Winterhalter​‌ supervises the PhD work​​ of Ewen Broudin-Caradec. He​​​‌ also co-advises, with Nicolas​ Tabareau and Matthieu Sozeau,​‌ the PhD of Yann​​ Leray who is located​​​‌ in the Gallinette team​ in Nantes.
• Catherine Dubois​‌ (thesis director) and Valentin​​ Blot (Gallinette team, Nantes)​​​‌ are supervising the PhD​ of Amélie Ledein (defense​‌ on February 10th 2026)​​
• Catherine Dubois and Burkhart​​​‌ Wolff (thesis director, LMF)​ are supervising the PhD​‌ of Benoit Ballenghien (defense​​ on December 18th 2025).​​​‌

9.2.4 Juries

• Frédéric Blanqui​ was in the PhD​‌ jury of Thibault Hilaire​​ on the certification in​​​‌ Rocq of covering algorithms​ for Petri nets,​‌ at the University of​​ Bordeaux, France.
• Frédéric Blanqui​​​‌ was in the PhD​ jury of Théo Laurent​‌ on structural subtyping in​​ Martin-Löf's type theory,​​​‌ at the University of​ Montpellier, France.
• Catherine Dubois​‌ was in the PhD​​ jury (reviewer) of Natan​​​‌ Talon on Automation of​ web application penetration testing,​‌ at CentraleSupélec, France.
• Bruno​​ Barras was in the​​​‌ PhD jury of Émile​ Oleon on Coherent Presentations​‌ of Groups in Homotopy​​ Type Theory, at Institut​​​‌ Polytechnique Paris, France.

International journals

• 13 article‌C.-C.Cezar-Constantin Andrici,‌​‌ D.Danel Ahman,​​ C.Cătălin Hriţcu,​​​‌ R.Ruxandra Icleanu,‌ G.Guido Martínez,‌​‌ E.Exequiel Rivas and​​ T.Théo Winterhalter.​​​‌ SecRef: Securely Sharing Mutable‌ References between Verified and‌​‌ Unverified Code in F​​.Proceedings of the​​​‌ ACM on Programming Languages‌9ICFPJuly 2025‌​‌, 510-540HALDOI​​back to text
• 14​​​‌ articleY.Yann Leray‌ and T.Théo Winterhalter‌​‌. Encode the Cake​​ and Eat it Too:​​​‌ Controlling computation in type‌ theory, locally.Proceedings‌​‌ of the ACM on​​ Programming Languages1062​​​‌January 2026HALDOI‌back to textback‌​‌ to text
• 15 article​​J.Johann Rosain,​​​‌ T.Tomás Díaz,‌ K.Kenji Maillard,‌​‌ M.Matthieu Sozeau,​​ N.Nicolas Tabareau,​​​‌ É.Éric Tanter and‌ T.Théo Winterhalter.‌​‌ Bounded Sort Polymorphism with​​ Elimination Constraints.Proceedings​​​‌ of the ACM on‌ Programming LanguagesJanuary 2026‌​‌HALback to text​​

International peer-reviewed conferences

• 16​​​‌ inproceedingsC.Claudio Sacerdoti‌ Coen, A.Abdelghani‌​‌ Alidra and F.Frédéric​​ Blanqui. The HOL-Light​​​‌ library of Multivariate Real‌ analysis in Rocq.‌​‌RocqPL 2026 - Rocq​​ for Programming LanguagesRennes,​​​‌ FranceJanuary 2026HAL‌back to text
• 17‌​‌ inproceedingsC.Claudio Sacerdoti​​ Coen and A.Abdelghani​​​‌ Alidra. Indexing and‌ Retrieval in a Heterogeneous‌​‌ Formal Library.CICM​​​‌ 2025 - 18th Conference​ on Intelligent Computer Mathematics​‌Brasilia, BrazilOctober 2025​​HALDOIback to​​​‌ text
• 18 inproceedingsG.​Geoff Sutcliffe, F.​‌Frédéric Blanqui and G.​​Guillaume Burel. Proof​​​‌ Verification with GDV and​ LambdaPi - It's a​‌ Matter of Trust.​​FLAIRS-3838Daytona Beach,​​​‌ FL, United StatesMay​ 2025HALDOIback​‌ to text
• 19 inproceedings​​T.Thomas Traversié.​​​‌ Monad Translations for Higher-Order​ Logic.Leibniz International​‌ Proceedings in Informatics (LIPIcs)​​FSCD 2025 - 10th​​​‌ International Conference on Formal​ Structures for Computation and​‌ Deduction33710th International​​ Conference on Formal Structures​​​‌ for Computation and Deduction​ (FSCD 2025)Birmingham, United​‌ KingdomSchloss Dagstuhl –​​ Leibniz-Zentrum für Informatik2025​​​‌HALDOIback to​ text
• 20 inproceedingsR.​‌Rishikesh Vaishnav. Lean4Less:​​ Eliminating Definitional Equalities from​​​‌ Lean via an Extensional-to-Intensional​ Translation.Theoretical Aspects​‌ of Computing – ICTAC​​ 2025 22nd International Colloquium​​​‌ICTAC 2025 - International​ Colloquium on Theoretical Aspects​‌ of ComputingLecture Notes​​ in Computer ScienceLNCS-16237​​​‌Marrakech, MoroccoNovember 2025​HALback to text​‌

National peer-reviewed Conferences

• 21​​ inproceedingsC.Catherine Dubois​​​‌. Domaines formellement vérifiés​.JFPC 2025 -​‌ Journées Francophones de Programmation​​ par ContraintesDijon, France​​​‌June 2025HALback​ to text

Doctoral dissertations​‌ and habilitation theses

• 22​​ thesisL.Luc Chabassier​​​‌. Aspects of category​ theory in proof assistants​‌.Université Paris-SaclayJuly​​ 2025HALback to​​​‌ text
• 23 thesisE.​Emilie Grienenberger. Combining​‌ computational theories.Université​​ Paris-SaclayFebruary 2025HAL​​​‌back to text

Reports​ & preprints

• 24 misc​‌C.Ciarán Dunne and​​ G.Guillaume Burel.​​​‌ Automatically Translating Proof Systems​ for SMT Solvers to​‌ the λΠ-calculus.November​​ 2025HALback to​​​‌ text
• 25 miscT.​Thiago Felicissimo and J.-P.​‌Jean-Pierre Jouannaud. Sort-Based​​ Confluence Criteria for Non-Left-Linear​​​‌ Higher-Order Rewriting.2025​HALback to text​‌
• 26 miscY.Yann​​ Leray, G.Gaëtan​​​‌ Gilbert, N.Nicolas​ Tabareau and T.Théo​‌ Winterhalter. The Rewster:​​ Type Preserving Rewrite Rules​​​‌ for the Rocq Prover:​ Extended version of the​‌ ITP 2024 paper.​​October 2025HALback​​​‌ to text
• 27 misc​T.Thomas Traversié.​‌ Kuroda's Translation for Higher-Order​​ Logic.November 2025​​​‌HALback to text​
• 28 miscT.Thomas​‌ Traversié and F.Florian​​ Rabe. Formalizing Representation​​​‌ Theorems for a Logical​ Framework with Rewriting.​‌April 2025HALback​​ to text