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