Deducteam

Deducteam is an INRIA research team that was founded by Gilles Dowek and is part of the LMF. We conduct research and develop tools for proof systems interoperability. More specifically:

We conduct research on logical frameworks (i.e. languages for representing the proofs of different proof systems) and, in particular, the λΠ-calculus modulo rewriting.
We develop the Dedukti proof checker and the Lambdapi proof assistant.
We study proof systems interoperability using Dedukti and Lambdapi, and develop various translators between existing proof assistants (Agda, HOL-Light, Isabelle, Lean, Rocq, etc.).
We study the alignment of mathematical concepts between the libraries of those systems, and develop tactics to automate the proofs of those alignments.
We develop tools to certify proofs generated by automated theorem provers and SMT solvers.
We work on the certification of proof transformations, and the termination and confluence of typed higher-order rewrite systems.

Deducteam led the COST action 20111 EuroProofNet.

Please consult our job list to see some internship/PhD/postdoc research topics we are interested in. More can be found on the web pages of Deducteam members.

If you would like to join Deducteam as a postdoc or a permanent researcher please contact us directly as well.

Activity reports

Recent papers and drafts ⟩ see all

Encode the Cake and Eat it Too

Yann Leray, Théo Winterhalter

Proceedings of the ACM on Programming Languages (2026)

Bounded Sort Polymorphism with Elimination Constraints

Johann Rosain, Tomás Díaz, Kenji Maillard, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter, Théo Winterhalter

Proceedings of the ACM on Programming Languages (2026)

The HOL-Light library of Multivariate Real analysis in Rocq

Claudio Sacerdoti Coen, Abdelghani Alidra, Frédéric Blanqui

RocqPL 2026 - Rocq for Programming Languages (2026)

Lean4Less: Eliminating Definitional Equalities from Lean via an Extensional-to-Intensional Translation

Rishikesh Vaishnav

ICTAC 2025 - International Colloquium on Theoretical Aspects of Computing (2025)

Automatically Translating Proof Systems for SMT Solvers to the λΠ-calculus

Ciarán Dunne, Guillaume Burel

(2025)