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@example.org, LMF, 4 avenue des Sciences, 91190 Gif-sur-Yvette