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

Proofs for Free in the λΠ-Calculus Modulo Theory

Thomas Traversié

LFMTP 2024 - International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (2024)

Kuroda's Translation for the λΠ-Calculus Modulo Theory and Dedukti

Thomas Traversié

LFMTP 2024 - International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (2024)

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)