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 and develop various translators between existing proof assistants (Agda, HOL-Light, Isabelle, Lean, Rocq, etc.) using Dedukti and Lambdapi.
- 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 between 2021 and 2025.
Please consult our job offers 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.