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: 47c1e0b49e389e04285abe5e54d5077d2fddbd07
Parent: efcbe24e146941712c5caac5db455bf38a938372
Author: Pablo <pablo-escobar@riseup.net>
Date: Mon, 9 Aug 2021 21:40:30 +0000

Implemented some suggestions from Thaago

Diffstat

2 files changed, 8 insertions, 4 deletions

Status	File Name	N° Changes	Insertions	Deletions
Added	main.pdf	0	0	0
Modified	sections/curry.tex	12	8	4

diff --git a/main.pdf b/main.pdf
Binary files differ.

diff --git a/sections/curry.tex b/sections/curry.tex
@@ -230,7 +230,7 @@
 
       \pause
 
-    \item A \emph{mathlib} nunca foi usada para provar algo novo\dots
+    \item A \emph{mathlib} ``nunca foi usada para provar algo novo''\dots
 
       \pause
 
@@ -258,13 +258,17 @@
             \item<5-> A prova de Mochizuki da conjetura abc
 
             \item<6-> A prova de Hales da conjectura de Kepler de 2015
+
+            \item<7->
+              \emph{\href{https://leanprover-community.github.io/liquid/}{Liquid
+              Tensor Experiment}}
           \end{itemize}
 
-        \item<7-> Limitações
+        \item<8-> Limitações
           \begin{itemize}
-            \item<7-> Cadê a intuição?
+            \item<8-> Cadê a intuição?
 
-            \item<8-> \emph{Who watches the Watchmen?} 
+            \item<9-> \emph{Who watches the Watchmen?} 
               \includegraphics[height=1em]{images/watchmen.eps}
           \end{itemize}
       \end{itemize}