Quick
index
main
eev
eepitch
maths
angg
blogme
dednat6
littlelangs
PURO
(C2,C3,C4,
 λ,ES,
 GA,MD,
 Caepro,
 textos,
 Chapa 1)

emacs
lua
(la)tex
maxima
git
lean4
agda
forth
squeak
icon
tcl
tikz
fvwm
debian
irc
contact

Lambda-cálculo 2023.1 - Eduardo Ochs

Links da aula de 04/jul:
Natural Numbers Game
Functional Programming in Lean4. Início pdfizado: FPLean4
Theorem Proving in Lean. PDF: TPinLean
Pelletier: A History of Natural Deduction. Fitch: PelletierP22
Minhas notas bagunçadas de quando eu fiz o curso do Francesco Noseda
Distributividade: (P&R)v(Q&R)→(PvQ)&R

Links da aula de 26/jun:
System F

Links da aula de 19/jun:
NG98 Nederpelt/Geuvers, p.69: Second Order Typed λ-calculus

Links da aula de 12/jun:
Adjunções: La2018p11, ZHAs4, MissingP26
Topologias como ordens parciais: ZHAs27, Rosiak186
O prefeixe malvado: MissingP57
Funtores: MissingP22
Transformações naturais: MissingP23
MissingP48 Y3 and Y4
Rosiak199 Yoneda Embedding

Links da aula de 05/jun:
Dois livros de Lógica Modal: MMM, Chellas
"Gnomes in the Fog ... Intuitionism in the 1920s": Hesseling

Links da aula de 15/maio:
Vamos tentar fazer os exercícios do La2018p8 até a p.16.
Dê uma olhada no Proofs and Types (capítulos 2 e 3).
La2018p17 / Planar HAs for children

Links da aula de 8/maio:
Vamos tentar fazer os exercícios do La2018p8 até a p.11.
Dê uma olhada aqui: SelingerP51 (até a p.55).


Essa optativa tem vários nomes.
O nome oficial dela é "λ-cálculo, lógicas e linguagens de programação".
Um nome melhor é "Lógicas, traduções e raciocício diagramático".
O código dela na UFF é RCN00049.
Ela vai ser nas 2as das 16:00 às 18:00 - veja aqui.

Fotos dos quadros: PDF, JPGs.
PDFzão com todos os PDFzinhos deste semestre.
Páginas de outros semestres:
2018.1, 2017.2, 2017.1, 2016.2, 2016.1, 2016

Sobre as reclamações do CAEPRO.
Um vídeo sobre didática: "Precisamos de mais slogans".
Os links curtos, como 3eT25 e Slogans08:54, estão explicados aqui.
Campanha: peçam pra eu voltar a dar Cálculo 3!


O curso vai ser principalmente sobre uma técnica pra entender coisas abstratas a partir de exemplos pequenos e sobre algumas aplicações dessa técnica: a gente vai aprender um pouco de λ-cálculo, Lógica, Teorias de Tipos, Categorias, e de algumas linguagens funcionais simples.

Aqui tem um vídeo e três artigos meus (dica: comece pelo vídeo!):

  • (slides, página, vídeo) Category Theory as An Excuse to Learn Type Theory (2021)
  • (PDF, página) On the Missing Diagrams in Category Theory (2022)
  • (PDF, página) Planar Heyting Algebras for Children (2017)
  • (PDF, página) Internal Diagrams and Archetypal Reasoning in Category Theory (2013)

A gente vai (tentar) ler alguns trechos destas notas sobre λ-cálculo,

e destes três livros de Categorias:

Aqui tem um monte de links sobre Teorias de Tipos.




O plano de curso no formato tradicional está aqui.
A versão detalhada com links está abaixo.

Aula 1 (03/abr, 7gQ1) Set comprehensions e notação λ.
Aula 2 (10/abr) feriado.
Aula 3 (17/abr, 7gQ3) Notação λ e redução.
Aula 4 (24/abr, 7gQ6) Exercícios de tipos.
Aula 5 (01/mai) feriado.
Aula 6 (08/mai, 7gQ8) Árvores; apagar e reconstruir informação.
Aula 7 (15/mai, 7gQ9) Curry-Howard e descarga de hipóteses.
Aula 8 (22/mai, 7gQ11) Exercícios de Planar Heyting Algebras.
Aula 9 (29/mai, 7gQ12) Dupla negação e De Morgan em ZHAs.
Aula 10 (05/jun, 7gQ13) Introdução à Logica Modal.
Aula 11 (12/jun, 7gQ16) Um pouco de categorias.
Aula 12 (19/jun, 7gQ21) Mais categorias.
Aula 13 (26/jun, 7gQ24) Algumas traduções.
Aula 14 (03/jul, 7gQ27) Um pouco de Lean (até o rw).
Aula 15 (10/jul)
Aula 16 (17/jul)

Grupo do Telegram: LA-C1-RCN-PURO-2023.1.