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

A Term-Patching Framework for Eliminating Definitional Equalities in Lean (Work-in-Progress)

Rishikesh Vaishnav

(2024)

PDFBibtex

Correct and Complete Type Checking and Certified Erasure for Coq, in Coq

Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Botsch Nielsen, Nicolas Tabareau, Théo Winterhalter

Journal of the ACM (JACM) (2024)

PDFBibtex

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