diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 22 |
1 files changed, 21 insertions, 1 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 7e4c691..aff8392 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -1828,6 +1828,13 @@ constructivisme russe de A. Markov fils) : resp. $\exists x.P(x)$ passe forcément par la preuve de $P$ ou de $Q$, resp. par la construction d'un $x$ vérifiant $P(x)$. +\bigskip + +\itempoint Les maths « normales » se font en logique classique, mais +certains bouts (explicit\textsuperscript{t} signalés comme tels) de la +littérature sont en logique intuitionniste. On peut y faire de +l'algèbre, de l'analyse, etc., constructives. + \end{frame} % \begin{frame} @@ -2149,7 +2156,7 @@ doute sur la correspondance elle-même. \end{frame} % \begin{frame} -\frametitle{Correspondance de Curry-Howard : exemple avec conjonction} +\frametitle{Correspondance de Curry-Howard : exemple avec disjonction} \itempoint Transformons en programme la démonstration qu'on a donnée de $A\lor B \Rightarrow B\lor A$ @@ -2218,6 +2225,19 @@ $\inferrule*[left={Void}]{\Gamma\vdash r:\bot}{\Gamma\vdash \itempoint Pas de nouvelle règle de réduction à ajouter. +\medskip + +{\footnotesize + +En OCaml : + +{\tt +type void = | ;; +let exfalso = fun (r:void) -> match r with \_ -> . ;; +} + +\par} + \end{frame} % \begin{frame} |