Quick
index
main
eev
maths
blogme
dednat4
littlelangs
PURO
(GAC2,
λ, etc)
(Chapa 1)

emacs
lua
(la)tex
fvwm
tcl
forth
icon
debian
irc
contact

Lambda-cálculo 2016.2 - Eduardo Ochs

Um PDF com todos os quadros de 2016.2 até agora:
http://angg.twu.net/2016.2-LA/2016.2-LA.pdf
Um PDF com todos os quadros do semestre anterior:
http://angg.twu.net/2016.1-LA/2016.1-LA.pdf

Material para exercícios:
http://angg.twu.net/LATEX/2016-2-LA-lambda.pdf
http://angg.twu.net/LATEX/2016-2-LA-logic.pdf
http://angg.twu.net/LATEX/2016-2-LA-cats.pdf
http://angg.twu.net/LATEX/2016-1-LA-material.pdf (antigo)

Fotos dos quadros:
http://angg.twu.net/2016.2-LA/20160906_LA1.jpg
http://angg.twu.net/2016.2-LA/20160913_LA1.jpg
http://angg.twu.net/2016.2-LA/20160920_LA1.jpg
http://angg.twu.net/2016.2-LA/20160927_LA1.jpg
http://angg.twu.net/2016.2-LA/20161004_LA1.jpg
http://angg.twu.net/2016.2-LA/20161011_LA1.jpg
http://angg.twu.net/2016.2-LA/20161011_LA2.jpg
http://angg.twu.net/2016.2-LA/20161025_LA1.jpg
http://angg.twu.net/2016.2-LA/20161101_LA1.jpg
http://angg.twu.net/2016.2-LA/20161108_LA1.jpg
http://angg.twu.net/2016.2-LA/20161108_LA2.jpg
http://angg.twu.net/2016.2-LA/20161122_LA1.jpg
http://angg.twu.net/2016.2-LA/20161122_LA2.jpg
http://angg.twu.net/2016.2-LA/20161129_LA1.jpg
http://angg.twu.net/2016.2-LA/20161129_LA2.jpg

30/ago/2016:
  Vieram a Marcela, o João Victor e o Neymar.
  Fizemos exercícios de redução, lambda-expressões e gráficos
  de funções; começamos a ver tipos. Esqueci de tirar fotos
  dos quadros. =(
 6/set/2016:
  Vieram a Marcela, o João Victor, o Juliano, o Victor e o Matheus.
  A gente terminou a aula usando a notação em árvore pra fazer
  exercícios de "type inference" e "term inference".
13/set/2016:
  Vieram o André, a Bruna, o Juliano, a Marcela, e o Matheus.
  Vimos um pouquinho de funções de duas variáveis, currying e
  uncurrying, depois vimos set comprehension (3 notações e
  exercícios), ZSets e notações posicionais.
20/set/2016:
  Vieram: André, Bruna, João Victor, Juliano, Marcela, Victor.
  Vimos as operações na lógica L_10 e como visualizá-las.
27/set/2016:
  Vieram: João Victor, Juliano, Marcela, e Matheus
 4/out/2016:
  Vieram: André, Bruna, João Victor, Juliano, Marcela, Matheus, Victor
11/out/2016:
  Vieram: André, João Victor, Juliano, Marcela, Matheus, Victor
  Composição e fatorações em Set.
18/out/2016:
  Não teve aula - foi semana acadêmica.
25/out/2016:
  Ninguém veio.
 1/nov/2016:
  Vieram: André, João Victor, Juliano, Marcela, Matheus, Victor
  Pedi pra todo mundo ler as pags 4 a 12 do Awodey:
  http://angg.twu.net/tmp/2016-optativa/awodey__category_theory.pdf
 8/nov/2016:
  Vieram: André, João Victor, Juliano, Marcela, Matheus
  Vimos terminais, iniciais e produtos em Set e em ordens parciais.
15/nov/2016:
  feriado
22/nov/2016:
  Vieram: André, João Victor, Juliano, Matheus, Victor
  Vimos coprodutos e a parte do Awodey sobre dualidade.
29/nov/2016:
  Vieram: André, João Victor, Juliano, Marcela, Matheus, Victor
  Vimos contextos, "|-" e as regras difíceis do lambda-bool-1.
 6/dez/2016:
  Vieram: André, João Victor, Juliano, Marcela, Victor
Páginas do semestre anterior:
http://angg.twu.net/2016-optativa.html
http://angg.twu.net/2016.1-LA.html
Programa (pro formulário 19):
Notação lambda para funções
Objetos matemáticos formados por números, conjuntos e listas
Funções e gráficos de funções
Diagramas de reduções para expressões
Tipos
Quantificadores
"Set comprehension"
Lógica
Tautologias
Lógicas como estruturas algébricas
Grafos direcionados
Ordens parciais

Outras estruturas algébricas: grupos, categorias
Ordens parciais como categorias
As categorias Set e FinSet
Produtos e exponenciais em Set e FinSet
Lambda-cálculo tipado em Set e FinSet
Variáveis livres
Categorias cartesianas fechadas ("CCCs")
Lambda-cálculo tipado em CCCs
Álgebras de Heyting planares ("ZHAs")
Lambda-cálculo tipado em ZHAs
Dedução Natural
O isomorfismo de Curry-Howard
Tautologias em ZHAs
Lógica intuicionista
Lógicas modais: S4
Semânticas para lambda-cálculo tipado
Árvores e Lisp
Semânticas para algumas linguagens de programação