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,
- Interoperability of proof systems using Dedukti,
- The λΠ-calculus modulo and Deduction modulo,
- Automated deduction in Deduction modulo,
- The termination and confluence of typed higher-order rewrite systems.
Activity reports: 2020, 2019, 2018, 2017, 2016, 2015, 2014, 2013, 2012.
Contact: Gilles Dowek, (first name).(last name)@inria.fr, LSV, 4 avenue des Sciences, 91190 Gif-sur-Yvette
