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: 4534b16417a9856acf686ce85c3b75fefa81e3cf
Parent: bf6ed36875c9ffb7c59dda8166df6976b7680ca6
Author: Pablo <pablo-escobar@riseup.net>
Date: Sun, 9 Oct 2022 23:45:22 +0000

Edited the slide pauses

Diffstat

1 file changed, 19 insertions, 22 deletions

Status	File Name	N° Changes	Insertions	Deletions
Modified	main.tex	41	19	22

diff --git a/main.tex b/main.tex
@@ -141,8 +141,6 @@
     \item Temos termos, mas não temos formulas!
   \end{itemize}
 
-  \pause
-
   \begin{figure}
     \centering
     \begin{tabular}{|l|l|}
@@ -168,8 +166,6 @@
     \item Objection!
   \end{itemize}
 
-  \pause
-
   \begin{columns}
     \begin{column}{.3\linewidth}
       \[
@@ -252,6 +248,8 @@
         \inputminted{c}{examples/typechecking.c}
       \end{figure}
 
+      \pause
+
     \item Linguagens estaticamente tipadas
   \end{itemize}
 
@@ -293,10 +291,12 @@
         \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}
+          \begin{figure}
+            \centering
+            \inputminted{lean}{examples/eq.lean}
+          \end{figure}
+
+          \pause
 
         \item O tipo \texttt{x = x} tem um único elemento \texttt{rfl}
       \end{itemize}
@@ -305,12 +305,11 @@
 
     \item O tipo \texttt{x = y} varia com \(x\) e \(y\)
 
-      \pause
-
     \item Tipos dependentes!
 
-    \item Codifico meus objetos como tipos
+      \pause
 
+    \item Codifico meus objetos como tipos
         \begin{figure}
           \centering
           \inputminted{lean}{examples/nat.lean}
@@ -382,8 +381,6 @@
     \end{column}
   \end{columns}
 
-  \pause
-
   \begin{figure}
     \centering
     \inputminted{lean}{examples/liquid.lean}
@@ -394,28 +391,28 @@
   \begin{columns}
     \begin{column}[t]{.65\linewidth}
       \begin{itemize}
-        \item<1-> Verificação formal de software e hardware \pause
+        \item<2-> Verificação formal de software e hardware \pause
           \begin{itemize}
-            \item<2-> O bug do Pentium de 1994
+            \item<3-> O bug do Pentium de 1994
 
-            \item<3-> A queda do voo 302 da Ethiopian Airlines em 2019
+            \item<4-> A queda do voo 302 da Ethiopian Airlines em 2019
           \end{itemize}
 
-        \item<4-> Provas de alta complexidade
+        \item<5-> Provas de alta complexidade
           \begin{itemize}
-            \item<4-> Classificação dos grupos simples finitos
+            \item<5-> Classificação dos grupos simples finitos
 
-            \item<5-> A prova de Mochizuki da conjetura abc
+            \item<6-> A prova de Mochizuki da conjetura abc
 
-            \item<6-> A prova de Hales da conjectura de Kepler de 2015!
+            \item<7-> A prova de Hales da conjectura de Kepler de 2015!
 
-            \item<7->
+            \item<8->
               A conclusão do
               \emph{\href{https://leanprover-community.github.io/liquid/}{Liquid
               Tensor Experiment}} em julho de 2022!
           \end{itemize}
 
-        \item<8-> \emph{Who watches the Watchmen?}
+        \item<9-> \emph{Who watches the Watchmen?}
           \includegraphics[height=1em]{images/watchmen.eps}
       \end{itemize}
     \end{column}