en ¦ fr > Formalizations

LogRel Coq

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.

Web Page GitHub

Under Creative Commons CC0 License, source on github. Built using Pelican. Theme adapted from pelican-svbhack by Giulio Fidente.