Type systems for logic.

1 files changed, 67 insertions, 1 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 60bef3a..c9269d5 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -468,6 +468,7 @@ linéarité.
 \end{frame}
 %
 \begin{frame}
+\label{typing-and-termination}
 \frametitle{Typage et terminaison}
 
 Un système de typage \alert{peut} garantir que \textbf{tout programme
@@ -543,7 +544,7 @@ restrictions :
 \item la logique concernée est plutôt « intuitionniste » (sans tiers
   exclu),
 \item diverses subtilités notamment dans la correspondance entre types
-  sommes paramétriques et $\exists$ côté logique.
+  sommes paramétriques (types $\Sigma$) et $\exists$ côté logique.
 \end{itemize}
 
 \end{frame}
@@ -596,4 +597,69 @@ tacite qu'on peut construire un tel $A$.
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Théories des types pour la logique (très bref aperçu)}
+
+\itempoint Langages spécialisés pour servir à la fois à l'écriture de
+programmes informatiques et de preuves mathématiques ; ils peuvent
+être soit sous forme de systèmes abstraits, soit sous forme
+d'implémentation informatique (« assistants de preuve » : Coq, Agda,
+Lean…).
+
+\bigskip
+
+\itempoint Dans tous les cas il s'agit de langages assurant la
+terminaison des programmes (cf. transp. \ref{typing-and-termination}),
+ou, dans le contexte du $\lambda$-calcul, la \emph{normalisation
+forte}.  Le type vide doit être inhabité !
+
+\bigskip
+
+Principales grandes familles (chacune avec énormément de variantes) :
+\begin{itemize}
+\item théories des types à la Martin-Löf (« MLTT ») : suit jusqu'au
+  bout la correspondance de Curry-Howard (\emph{aucune} distinction
+  entre types et propositions ; {\footnotesize pas de $\exists$ mais
+    plutôt un $\Sigma$}), $\rightarrow$ Agda ;
+\item variantes du « calcul des constructions » (« CoC »),
+  $\rightarrow$ Coq ;
+\item théorie homotopique des types (« HoTT ») : « égalité = isomorphisme ».
+\end{itemize}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Le $\lambda$-cube de Barendregt (très bref aperçu)}
+
+Il s'agit d'un ensemble de $8 = 2^3$ théories des types pour la
+logique : la plus faible est le « $\lambda$-calcul simplement typé »
+($\lambda_\rightarrow$, décrit plus loin), la plus forte le « calcul
+des constructions » (« CoC »).
+
+\medskip
+
+Chaque théorie du cube est caractérisée par l'absence ou la présence
+de chacune des $3$ fonctionnalités suivantes ($\lambda_\rightarrow$
+n'a aucune des trois, CoC a les trois) :
+
+\begin{itemize}
+\item \textcolor{blue}{termes pouvant dépendre de types}, ou
+  polymorphisme paramétrique « explicitement quantifié » (p.ex. $\prod
+  t.\; (t \rightarrow t)$) ;
+\item \textcolor{blue}{types pouvant dépendre de types}, ou
+  constructeurs de types ;
+\item \textcolor{blue}{types pouvant dépendre de termes}, ou « types
+  dépendants », correspondant côté logique à la quantification sur les
+  individus.
+\end{itemize}
+
+\medskip
+
+{\footnotesize On peut ensuite encore ajouter des fonctionnalités :
+  par exemple, Coq est basé sur le « calcul des constructions
+  inductives » qui ajoute au calcul des constructions des mécanismes
+  systématiques pour former des types (positivement !) récursifs.\par}
+
+\end{frame}
+%
 \end{document}