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: d315704b2ab970569c48bd7e1dd63a02b4879bba
Parent: 9f558c5dd7796f822264eb41f619d8ba15efa2b3
Author: Pablo <pablo-escobar@riseup.net>
Date: Thu, 13 Oct 2022 22:09:14 +0000

Updated the README

Diffstat

1 file changed, 3 insertions, 51 deletions

Status	File Name	N° Changes	Insertions	Deletions
Modified	README.md	54	3	51

diff --git a/README.md b/README.md
@@ -1,52 +1,4 @@
-# Plano
-
-* Disclaimers
-* Provas numéricas
-  * Ideia
-    * Provar coisas as vezes são continhas
-    * Compudores são bons em vazer continhas
-    * Podemos usar eles
-  * Exemplo daquele paper de combinatória
-  * Exemplo mais básico?
-* Provadores de teoremas
-  * Ideia
-    * Provar coisas as vezes são continhas, não só continhas aritmeticas, mas
-      continhas "lógicas"
-    * Indução por exemplo é continha
-    * Computadores são bons com continhas
-    * Podemos usar eles?
-  * Primeira ideia
-    * Usar boolans e checar todos os casos?
-    * Não rola se eu tenho infinitos casos
-  * Como eu faço então? Tento representar as afirmações lógicas no computador
-  * Problema: temos termos mas não temos formulas
-  * Solução: curry howard
-  * Mas como eu passo isso pra um PC?
-    * Preciso de uma linguagem estaticamente tipada: provar uma coisa significa
-      contruir um elemento do tipo correspondente, então precisamos garantir
-      que esse elemento é de fato do tipo correspondente
-    * Fixo coisas que eu quero impor que são verdade
-    * Exemplo: fixo que x = x
-    * Pra isso eu preciso de tipos dependentes
-  * Exemplos de provadores de teoremas: Lean, Idris, Coq?, Agda?
-  * Algum exemplo básico em Lean
-  * Isso é meio que inútil
-    * Não tamos ainda na posição de provar novos resultados em Lean, mas só de
-      "verificar formalmente" que resultados já provados são verdade
-    * Exemplo do paper de combinatória
-    * Do que adianta ter uma prova formal se não temos um real entendimento de
-      por que aquilo é verdade?
-* Uso exploratório
-  * Ideia
-    * As vezes entender casos particulares ou desenhar as coisas ajuda muito a
-      gente a entender o caso geral
-    * Mas provar casos particulares/desenhar as coisas pode envolver muitas
-      continhas chatas
-    * Computadores são bons em continhas
-    * Podemos usar eles
-  * Manipulação simbólica
-    * Exemplo de integração simbólica
-    * Exemplo de "x + 2" em Python vs. Mathics?
-    * CAS
-  * Exemplos de CAS: SageMath, Gap, Mathics?
+# Curry-Howard
 
+Slides of a (very) informal lecture of mine on the Curry-Howard correspondence
+on the S4 group.