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

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

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

International Conference on Interactive Theorem Proving (ITP 2024) (2024)

Dependent Ghosts Have a Reflection for Free

Théo Winterhalter

Proceedings of the ACM on Programming Languages (2024)

Proofs for Free in the λΠ-Calculus Modulo Theory

Thomas Traversié

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

A toy model provably featuring an arrow of time without past hypothesis

Pablo Arrighi, Gilles Dowek, Amélia Durbec

International Conference on Reversible Computation (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)