2026 team photo

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:

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.

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)

Sulfur: a Reflective Tactic for Substitution Simplification

Mathis Bouverot-Dupuis, Théo Winterhalter, Kathrin Stark, Kenji Maillard

RocqPL 2026 - Rocq for Programming Languages (2026)