A (humorous) graphical representation of the Curry-Howard correspondence.

3 files changed, 27 insertions, 4 deletions

diff --git a/images/sean-connery-in-name-of-the-rose.jpg b/images/sean-connery-in-name-of-the-rose.jpg
new file mode 100644
index 0000000..2f24fdb
--- /dev/null
+++ b/images/sean-connery-in-name-of-the-rose.jpg
diff --git a/images/sean-connery-in-zardoz.jpg b/images/sean-connery-in-zardoz.jpg
new file mode 100644
index 0000000..e3d81fb
--- /dev/null
+++ b/images/sean-connery-in-zardoz.jpg
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 0d0443d..6e21de5 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -545,8 +545,8 @@ Exemple de tel langage : Coq.
 Idée générale : établir une analogie, voire une correspondance précise
 entre
 \begin{itemize}
-\item \textbf{types} et \textbf{termes} de ces types dans un système
-  de typage,
+\item \textbf{types} et \textbf{termes} (=programmes) de ces types
+  dans un système de typage,
 \item \textbf{propositions} et \textbf{preuves} de ces propositions
   dans un système logique.
 \end{itemize}
@@ -569,8 +569,9 @@ P.ex., la preuve évidente de l'affirmation $(A \land B) \Rightarrow A$
 Beaucoup de variations sur cette correspondance, mais il y a des
 restrictions :
 \begin{itemize}
-\item le langage informatique doit garantir la terminaison, sinon cela
-  reviendrait à permettre les preuves circulaires,
+\item le langage informatique doit garantir la terminaison (pas
+  d'appels récursifs !), sinon cela reviendrait à permettre les
+  preuves circulaires,
 \item la logique concernée est plutôt « intuitionniste » (sans tiers
   exclu),
 \item diverses subtilités notamment dans la correspondance entre types
@@ -580,6 +581,28 @@ restrictions :
 \end{frame}
 %
 \begin{frame}
+\frametitle{La correspondance de Curry-Howard (illustration graphique)}
+
+\begin{center}
+\begin{tabular}{c@{\hskip 30bp}c}
+\includegraphics[height=150bp]{images/sean-connery-in-name-of-the-rose.jpg}
+&\includegraphics[height=150bp]{images/sean-connery-in-zardoz.jpg}
+\\
+Preuves mathématiques&Programmes informatiques
+\\
+{\footnotesize (contemplatives ?)}&{\footnotesize (dynamiques ?)}
+\end{tabular}
+
+\bigskip
+
+On a du mal à le croire, mais c'est la même chose !
+
+{\footnotesize (N.B. : ne pas prendre ce résumé simpliste trop au sérieux.)\par}
+\end{center}
+
+\end{frame}
+%
+\begin{frame}
 \frametitle{La correspondance de Curry-Howard (premier aperçu)}
 
 {\footnotesize\textcolor{gray}{Divulgâchis pour la suite !}\par}