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

Translating HOL-Light proofs to Coq

Frédéric Blanqui

LPAR-25 - 25th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (2024)

From Rewrite Rules to Axioms in the λΠ-Calculus Modulo Theory

Valentin Blot, Gilles Dowek, Thomas Traversié, Théo Winterhalter

FoSSaCS 2024 - 27th International Conference on Foundations of Software Science and Computation Structures (2024)

The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant

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