Deducteam is an INRIA research team of the Programs, Verification and Proofs theme located at the LSV.
See our internship and PhD subject proposals!
We conduct research on proof processing systems and more specifically on:
- Dedukti, a backend for various proof systems based on the λΠ-calculus modulo rewriting,
- Interoperability of proof systems using Dedukti,
- The λΠ-calculus modulo rewriting and Deduction Modulo,
- Automated deduction in Deduction modulo,
- The termination and confluence of typed higher-order rewrite systems.
Deducteam is strongly involved in the COST action 20111 EuroProofNet.
Contact: Gilles Dowek, firstname.lastname@inria.fr, LMF, 4 avenue des Sciences, 91190 Gif-sur-Yvette
