From 66c7935fab7982a8a18fa63a53dc349fe65eed0e Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Tue, 12 Dec 2023 16:07:20 +0100
Subject: A brief word on Curry-Howard for sequent calculus, and the
 lambda-bar-calculus.

---
 transp-inf110-02-typage.tex | 62 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 62 insertions(+)

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index cd3857a..980d0b5 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -3116,6 +3116,68 @@ $Q$.  {\footnotesize (\underline{Preuve :} c'est clair sur chacune des
   coupure), et répéter jusqu'à ce que le séquent recherché ait été
   marqué ou que plus aucun séquent ne soit marqué.\qed\par}
 
+\end{frame}
+%
+\begin{frame}
+\frametitle{Calcul des séquents et Curry-Howard}
+
+\itempoint On a vu que les preuves en déduction naturelle
+correspondent aux termes du $\lambda$-calcul simplement typé
+(+extensions).
+
+\smallskip
+
+On peut trouver un correspondant aux preuves en calcul des séquents
+{\footnotesize (avec de petites modifications)} : le
+$\overline{\lambda}$-calcul de Herbelin.
+
+\smallskip
+
+{\footnotesize Le $\overline{\lambda}$-calcul a deux sortes d'objets :
+  les \emph{termes} $t$ et les \emph{listes d'arguments} (notées
+  $[t_1;\ldots;t_r]$).\par}
+
+\medskip
+
+\itempoint En travaillant un peu, on peut déduire l'élimination des
+coupures de la conversion en $\overline{\lambda}$-calcul de termes
+normaux du $\lambda$-calcul (donc de sa normal\textsuperscript{ion}).
+
+\begin{center}
+\scalebox{0.56}{
+$\inferrule*{
+\inferrule*{
+\inferrule*{ }{y : C\vdash y : C}
+\\
+\inferrule*{ }{x_1:A_1\vdash x_1 : A_1}
+}{y:C, x_1:A_1\vdash yx_1 : A_2\to B}
+\\
+\inferrule*{ }{x_2:A_2\vdash x_2 : A_2}
+}{y:C, x_1:A_1, x_2:A_2\vdash yx_1 x_2 : B}$
+}
+$\rightsquigarrow$
+\scalebox{0.56}{
+$\inferrule*{
+\inferrule*{
+\inferrule*{ }{x_1:A_1\vdash x_1:A_1}
+\\
+\inferrule*{
+\inferrule*{ }{x_2:A_2\vdash x_2:A_2}
+\\
+\inferrule*{ }{\_:C \vdash \_ [] : C}
+}{x_2:A_2;\_:A_2\to B \vdash \_ [x_2] : A_2\to B}
+}{x_1:A_1, x_2:A_2;\_:C \vdash \_ [x_1; x_2] : B}
+}{y:C, x_1:A_1, x_2:A_2\vdash y [x_1; x_2] : B}$
+}
+
+\footnotesize
+
+(où $C := A_1\to A_2 \to B$)
+
+(à gauche le $\lambda$-calcul, à droite le
+$\overline{\lambda}$-calcul ; remarquez l'inversion des arguments)
+\end{center}
+
 \end{frame}
 %
 % TODO:
-- 
cgit v1.2.3