From 9587f8530a6eeb37bb81f530dbc0848162eaf11b Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Fri, 24 Nov 2023 11:15:07 +0100
Subject: A (humorous) graphical representation of the Curry-Howard
 correspondence.

---
 images/sean-connery-in-name-of-the-rose.jpg | Bin 0 -> 40619 bytes
 images/sean-connery-in-zardoz.jpg           | Bin 0 -> 60245 bytes
 transp-inf110-02-typage.tex                 |  31 ++++++++++++++++++++++++----
 3 files changed, 27 insertions(+), 4 deletions(-)
 create mode 100644 images/sean-connery-in-name-of-the-rose.jpg
 create mode 100644 images/sean-connery-in-zardoz.jpg

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
Binary files /dev/null and b/images/sean-connery-in-name-of-the-rose.jpg differ
diff --git a/images/sean-connery-in-zardoz.jpg b/images/sean-connery-in-zardoz.jpg
new file mode 100644
index 0000000..e3d81fb
Binary files /dev/null and b/images/sean-connery-in-zardoz.jpg differ
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,14 +569,37 @@ 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
   sommes paramétriques (types $\Sigma$) et $\exists$ côté logique.
 \end{itemize}
 
+\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}
-- 
cgit v1.2.3