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)

PDFBibtex

Dependent Ghosts Have a Reflection for Free

Théo Winterhalter

Proceedings of the ACM on Programming Languages (2024)

PDFBibtex

Computer-Assisted Proof Verification for Higher-Order Automated Reasoning within the Dedukti Framework, Vérification de preuves assistée par ordinateur pour le raisonnement automatisé d'ordre supérieur dans le cadre de Dedukti

Melanie Taprogge

(2024)

PDFBibtex

Proofs for Free in the λΠ-Calculus Modulo Theory

Thomas Traversié

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

PDFBibtex

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

Pablo Arrighi, Gilles Dowek, Amélia Durbec

RC 2024 - 16th International Conference on Reversible Computation (2024)

PDFBibtex