Term inference for Dedukti Gaëtan Gilbert, supervised by Arnaud Spiwack,

The general context Dedukti is an experimental language designed to write proof checkers for various logics. It is used to implement independent proof checkers for proof assistants such as Coq and Isabelle and trace checkers for automated deduction tools such as Zenon and iprover modulo. The logic underlying Dedukti is called λΠ-modulo: it is an extension of λΠ, the simplest form of dependently typed λ-calculus (also called λP), with user-defined rewriting rules for type equality (a.k.a. conversion) [5]. The research problem Dedukti proofs require information to be made explicit when it could be deduced from the rest of the proof. This makes writing and reading real world proofs difficult. Proof assistants such as Coq solve this problem by inserting a term in-ference phase before type checking. Given its small code base and low re-quirements for backward compatibility, Dedukti provides an opportunity t