1 files changed, 40 insertions, 0 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 3a6a49a..8cc025c 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -2419,6 +2419,44 @@ $\Rightarrow$ comme interchangeables.
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{La négation et la double négation}
+
+\textcolor{orange}{Qu'est-ce qui correspond à la proposition $\neg P$
+  par Curry-Howard ?}
+
+\medskip
+
+C'est le type $\sigma \rightarrow 0$ des fonctions prenant un argument
+de type $\sigma$ et renvoyant une valeur impossible, i.e., ne peuvent
+jamais renvoyer.
+
+\medskip
+
+Mais on parle d'un langage ($\lambda$CST enrichi) où \alert{tous les
+  programmes terminent} (« normalisation forte ») !  Donc une telle
+fonction prouve que $\sigma$ est lui-même vide ; et la fonction est
+triviale : c'est une « pure preuve » de vacuité de $\sigma$ :
+
+\smallskip
+
+\begin{itemize}
+\item le type $\sigma \rightarrow 0$ (ou « $\neg\sigma$ ») est le type
+  des « témoignages de vacuité » de $\sigma$ \textcolor{teal}{(si on
+    me fournit un truc de type $\sigma$, je soulève une exception
+    parce que c'est impossible)},
+\item le type $(\sigma \rightarrow 0) \rightarrow 0$ (ou
+  « $\neg\neg\sigma$ ») est une sorte de type des témoignages de
+  \alert{non-vacuité} de $\sigma$,
+\item mais ce dernier ne permet pas « magiquement » d'en tirer une
+  valeur :
+\item pas de terme de type $((\alpha \rightarrow 0) \rightarrow 0) \to
+  \alpha$ ou bien $\alpha + (\alpha\rightarrow 0)$ dans le
+  $\lambda$CST : on est bien en \alert{logique intuitionniste}.
+\end{itemize}
+
+\end{frame}
+%
 % TODO:
 % - discussion de la négation et double négation
 % - substitution des variables propositionnelles par des formules
@@ -2426,6 +2464,8 @@ $\Rightarrow$ comme interchangeables.
 % - présentation en calcul des séquents
 % - élimination des coupures
 % - Kripke
+% - fragment négatif
+% - call/cc
 % - inférence de type de Hindley-Milner
 %
 \end{document}