Deducteam

Deducteam is strongly involved in the COST action 20111 EuroProofNet.

Please consult our job list to see various internship offers we had recently. You can also contact us directly if there is a topic we work on you would find interesting, even if it's not listed there.

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

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)

PDFBibtex

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

Rishikesh Vaishnav

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

PDFBibtex

Kuroda's Translation for Higher-Order Logic

Thomas Traversié

(2025)

PDFBibtex

Indexing and Retrieval in a Heterogeneous Formal Library, Indexation et recherche dans une bibliothèque formelle hétérogène

Claudio Sacerdoti Coen, Abdelghani Alidra

CICM 2025 - 18th Conference on Intelligent Computer Mathematics (2025)

PDFBibtex

The Rewster: Type Preserving Rewrite Rules for the Rocq Prover

Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, Théo Winterhalter

(2025)

PDFBibtex