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.
Contact: Gilles Dowek, (first name).(last name)@inria.fr, LSV, 4 avenue des Sciences, 91190 Gif-sur-Yvette