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: 596f7cf48b1acaa1677bfff26c893eab465ba774
Parent: 15c4e7c021c3675286035ae8c4c0d0fdb14cb535
Author: Pablo <pablo-escobar@riseup.net>
Date: Sun, 9 Oct 2022 20:17:38 +0000

Added a disclaimer on natural deduction

Diffstat

2 files changed, 41 insertions, 13 deletions

Status	File Name	N° Changes	Insertions	Deletions
Modified	examples/hacker.txt	18	5	13
Modified	main.tex	36	36	0

diff --git a/examples/hacker.txt b/examples/hacker.txt
@@ -1,13 +1,5 @@
-00110000100011101000011100011010111110101010011000
-00010011011001101011110011011101011010000101010110
-10111101100000110001110010100000101100111110100000
-01001110001000101000110010000001100010001100110110
-00100110000010011010010100000110101110110000101101
-11011111111010010100110100001110100110001111001110
-10101000000101000000000100101000000110001011001010
-11001000101110010001010000101101001110110011100101
-01010100011110010001010000111010101010000011001111
-01100010111011110001111101011011100010000101111100
-11011110010011011110001100010101110110100100100000
-10110010101101110111101110100101111011001111001111
-10100001010100010010111100001010011000010110111110
+0001001101100110101111001101110101101000010101011
+1011110110000011000111001010000010110011111010000
+0100111000100010100011001000000110001000110011011
+0010011000001001101001010000011010111011000010110
+1101111111101001010011010000111010011000111100111

diff --git a/main.tex b/main.tex
@@ -28,6 +28,42 @@
 
       \pause
 
+      \pause
+
+    \item Dedução natural\dots
+      \[
+        \begin{array}{cc}
+          \displaystyle{
+            \frac{\Gamma \vdash_\Sigma a : A \quad \Gamma \vdash_\Sigma b : B}
+                 {\Gamma \vdash_\Sigma \operatorname{intro} a \ b : A \wedge B}
+            \rightarrow C
+          } &
+          \displaystyle{
+            \frac{
+              \Gamma \vdash_\Sigma a : A \quad
+              \Gamma \vdash_\Sigma f : A \supset B
+            }{\Gamma \vdash_\Sigma f a : B}
+            \rightarrow E
+          } \\ \\
+          \displaystyle{
+            \frac{\Gamma \vdash_\Sigma a : A}
+                 {\Gamma \vdash_\Sigma \operatorname{inl} a : A \vee B}
+            \rightarrow D_1
+          } &
+          \displaystyle{
+            \frac{\Gamma \vdash_\Sigma b : B}
+                 {\Gamma \vdash_\Sigma \operatorname{inr} b : A \vee B}
+            \rightarrow D_2
+          }
+        \end{array}
+     \]
+
+      \pause
+
+    \item Não precisa entender o código!
+
+      \pause
+
     \item Me interrompa!
   \end{itemize}
 \end{frame}