|
|
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.
|