A project to show decidability of type-checking for a dependently-typed language, featuring all representative features of Martin-Löf Type Theory. Logical relation setup heavily inspired by a previous similar project in Agda.

Started as Arthur's internship subject. I took over at the end of it and developed a large part of the project, especially the later algorithmic parts and decision algorithm. Kenji and Loïc contributed too, mainly around the logical relation.

A project formalizing Coq in Coq and providing tools for manipulating Coq terms and developing certified plugins (i.e. translations, compilers or tactics) in Coq.

I contributed mostly on the theory part, more specifically to the proof of completeness of the type-checker that is implemented as part of the project, through an equivalence between the specification and a bidirectional type system reflecting the implementation.