curry-howard

Slides of a (very) informal lecture of mine on the Curry-Howard correspondence

git clone: git://git.pablopie.xyz/curry-howard
Log
Files
Refs
README
LICENSE

Commit: 15c4e7c021c3675286035ae8c4c0d0fdb14cb535
Parent: 062b330571c0f0fae1dbb73b71dcfb314989197e
Author: Pablo <pablo-escobar@riseup.net>
Date: Sun, 9 Oct 2022 19:26:07 +0000

Continued to rework the section on the Curry-Howard correspondance

Diffstat

6 files changed, 53 insertions, 7 deletions

Status	File Name	N° Changes	Insertions	Deletions
Added	examples/eq.lean	4	4	0
Modified	examples/fake-theorem.py	1	0	1
Added	examples/nat.lean	3	3	0
Modified	examples/typechecking.c	2	1	1
Added	examples/types.lean	7	7	0
Modified	sections/curry.tex	43	38	5

diff --git a/examples/eq.lean b/examples/eq.lean
@@ -0,0 +1,4 @@
+inductive Eq (x : t) (y : t) : Prop
+| rfl : Eq x x
+
+infix = := Eq

diff --git a/examples/fake-theorem.py b/examples/fake-theorem.py
@@ -1,2 +1 @@
 f(n + m) % (f(n) * f(m)) == 0
-

diff --git a/examples/nat.lean b/examples/nat.lean
@@ -0,0 +1,3 @@
+inductive Nat : Type 
+| zero : Nat
+| succ : Nat → Nat

diff --git a/examples/typechecking.c b/examples/typechecking.c
@@ -5,5 +5,5 @@ unsigned int f(unsigned int n)
 }
 
 // error: implicit conversion from 'float' to 
-// 'unsigned int' changes value from 0.5 to 0
+// 'unsigned int'
 f(0.5f);

diff --git a/examples/types.lean b/examples/types.lean
@@ -0,0 +1,7 @@
+-- a e b <-> And a b
+inductive And (a : Prop) (b : Prop) : Prop
+| intro : a → b → And a b
+
+inductive Or (a : Prop) (b : Prop) : Prop
+| inl : a → Or a b
+| inr : b → Or a b

diff --git a/sections/curry.tex b/sections/curry.tex
@@ -169,13 +169,37 @@
   \end{center}
 \end{frame}
 
-\begin{frame}{Provadores de Teoremas}
+\begin{frame}{A Correspondência de Curry-Howard}
   \begin{itemize}
-    \item Fixo certas coisas que quero impor que sejam verdade
+    \item Mas como isso funciona na prática?
+        \begin{figure}
+          \centering
+          \inputminted{python}{examples/types.py}
+        \end{figure}
+
+        \pause
+
+        \begin{figure}
+          \centering
+          \inputminted{lean}{examples/types.lean}
+        \end{figure}
+
+    \item Tipos algébricos!
+  \end{itemize}
+\end{frame}
+
+\begin{frame}{A Correspondência de Curry-Howard}
+  \begin{itemize}
+    \item Aximas!
       \begin{itemize}
         \item Dados \(x\) e \(y\), existe o tipo \texttt{x = y} das provas de
           que \(x = y\)
 
+        \begin{figure}
+          \centering
+          \inputminted{lean}{examples/eq.lean}
+        \end{figure}
+
         \item O tipo \texttt{x = x} tem um único elemento \texttt{rfl}
       \end{itemize}
 
@@ -185,11 +209,20 @@
 
       \pause
 
-    \item Tipos dependentes
+    \item Tipos dependentes!
 
-      \pause
+    \item Fixo alguns tipos primitivos
+
+        \begin{figure}
+          \centering
+          \inputminted{lean}{examples/nat.lean}
+        \end{figure}
+  \end{itemize}
+\end{frame}
 
-    \item Provadores de Teoremas
+\begin{frame}{Provadores de Teoremas}
+  \begin{itemize}
+    \item Provadores de Teoremas!
       \begin{itemize}
         \item Coq (\url{https://coq.inria.fr/})