My thesis Extending Type Theory with Syntactical Models is available here.
It comes with several formalizations gathered in this repository: https://gitlab.inria.fr/sboulier/thesis-formalizations
Changelog
6-Aug-2018 : first release
24-Aug-2018 : typos
10-Sept-2018 : links in Section 5
28-Sept-2018 : add cover and abstract, few typos corrected in the introduction
15-Nov-2018 : abstract and numberring of sections corrected
9-Jan-2019 : correcting some remarks of the jury