small post-defence corrections

Author: MevenBertrand

Abstract.md

@@ -1,6 +1,8 @@
 Typage Bidirectionnel pour le Calcul des Constructions Inductives
 ===
 
+Mots clés : Théorie des Types, Assistants à la Preuve, Typage Bidirectionnel, Calcul des Constructions Inductives, Coq, Typage Graduel
+
 Durant leurs plus de 50 ans d'existence, les assistants à la preuve
 se sont établis comme des outils permettant un haut niveau
 de fiabilité dans de nombreuses applications.
@@ -27,16 +29,18 @@ du typage dynamique et constitue la dernière partie de la thèse.
 Bidirectional Typing for the Calculus of Inductive Constructions
 ===
 
+Keywords: Type Theory, Proof Assistant, Bidirectional Typing, Calculus of Inductive Constructions, Coq, Gradual Typing
+
 Over their more than 50 years of existence, proof assistants have established themselves as
 tools guaranteeing high trust levels in many applications.
 Yet, due to their increasing complexity, the historical solution of relying on a
-small, trusted kernel is not enough anymore to avoid critical bugs while moving forward.
+small, trusted kernel is not enough any more to avoid critical bugs while moving forward.
 But proof assistants have been used for decades to certify program correctness,
 so why not their own?
 This is the ambition of the MetaCoq project,
 which aims at providing the first realistic kernel for a proof assistant – Coq –
 to be formally proven correct, in Coq itself.
-Don't trust the program anymore, only its proof!
+Don't trust the program any more, only its proof!
 
 This thesis studies the bidirectional structure on which the typing algorithm
 implemented by the kernel of Coq relies, in the context of the Calculus of

Manuscript/biblio.bib

@@ -2673,7 +2673,7 @@ @Book{Begriffsschrift
   publisher  = {Halle a.d.S.: Louis Nebert},
   groups     = {History},
   priority   = {prio3},
-  shorttitle = {Begriffsschift},
+  shorttitle = {Begriffsschrift},
 }
 
 @Book{Hales2012,

Manuscript/bidir-intro.tex

@@ -9,7 +9,7 @@
 sensible mode fails, indicating they are not suited for an implementation.
 In the case of the typing judgement $\Gamma \vdash t \ty T$,
 usually both the term $t$ under inspection and the context $\Gamma$ are inputs –
-although some depart from this \sidetextcite{Jim1996}.
+although some depart from this \sidecite{Jim1996}.
 The mode of the type $T$, however, is much less clear: should it be inferred based upon
 $\Gamma$ and $t$, or do we merely want to check whether $t$ conforms to a given $T$?
 Both are sensible questions, and in fact typing algorithms for complex type systems usually 

Manuscript/intro-fr.tex

@@ -489,7 +489,7 @@ \section{\kl{Coq} et son noyau}
 et leur vérification est effectuée par un algorithme proche
 de ceux utilisés pour les types des langages conventionnels.
 Cependant, si, dans les premières versions des années 80, les preuves \kl{Coq} étaient
-écrite quasiment directement en \kl{Gallina},
+écrites quasiment directement en \kl{Gallina},
 ce n’est actuellement plus du tout le cas.
 La raison est que la majeure partie de l’outil dans ses versions actuelles a
 pour but d’aider l’utilisatrice à générer une preuve correcte. C’est un véritable

Manuscript/technical-intro.tex

@@ -444,7 +444,7 @@ \section{50 Shades of Conversion}
 In the rest of this section we give two presentations of \kl{untyped conversion}.
 First, a \kl(conv){declarative} one, which we use to define \kl{CCω}, as is standard.
 Second, an \kl(conv){algorithmic} one, anticipating the need for it later on
-in Parts \refname{metacoq} and \refname{gradual}.
+in Parts \nameref{part:metacoq} and \nameref{part:gradual}.
 % in \arefpart{metacoq} where it is used to show decidability of type-checking, and
 % in \arefpart{gradual}, where we extend it into a relation that is by design not transitive, so
 % that basing it on declarative conversion would be nonsensical.