Official deposit version

Version used for official institutional deposit at the University of Nantes.

Post-defence version

Minor typos correction and editing of the cover after the defence.

Defence Version

Added the acknowledgments, and the feedback from the rapporteurs.

Adding the missing chapter

Complete version, with the missing chapter 6 filled in.

Minor correction to v1.0

Fixing Jesper Cockx’s status in the cover.

First official release

First official, complete release. Chapter 6 (bidirectional conversion) is still missing.

Finished MetaCoq part

The second MetaCoq chapter, on formalization of bidirectional typing, is added. As usual, there’s also some more polishing.

Formalized Meta-Theory

The main addition the first chapter on MetaCoq. Extra bonuses include proof-reading by various people, the proper formatting including MathSTIC cover.

Finished Gradual Part, and Front Matter

Added the missing gradual chapter, and the How-To and Abstract.

Translated Introduction

Added chapter 2 (general introduction, translation of chapter 1 in English), and some small-scale polishing here and there.