Provas Formais: Uma Introdução à Teoria de Tipos

Table of Contents

1 Quadro de Avisos

1.1 [2017-08-21 Seg 09:57]: Notas de aula (pdf)

1.2 [2017-08-09 Qua 15:24]: As aulas a partir desta sexta-feira [2017-08-11 Sex] serão realizadas no LINF 4.

1.3 Apresentação da disciplina (pdf)

2 Quadro de notas:

Matrícula Faltas(*) Faltas (%) Ex1(12) Ex2(15) Nat(10) List Sort Menção
100109829 3 10.00            
110146123 1 3.33 12 15        
120049031 2 6.67   14 8      
120050943 1 3.33 12 15 5      
120126443 2 6.67 11 13        
140153641 1 3.33 12 13 7      
140160299 0 0.00 12 15 10      
150014961 2 6.67 12 15 5      
150021623 2 6.67 12 15 7      
150023928 2 6.67 12 15 4      
150126689 2 6.67 12 15 6      
150143290 4 13.33 12 15 10      
150143362 2 6.67 12 15 10      
160003318 5 16.67   13 5      
160005809 5 16.67 12 15        
170043339 12 40.00           SR

(*) Última atualização: [2017-09-15 Sex 14:13]

3 Calendário de aulas:

  1. [2017-08-07 Seg 12:00]–[2017-08-07 Seg 13:50] Tipos Simples ✓
    • O fragmento implicacional da lógica proposicional intuicionista
    • Exercícios:
      • Arquivo coq: exercicio1.v
        • A solução dos exercícios deve ser enviada para contato@flaviomoura.mat.br
        • Assunto do email: [pftt] Exercício 1
        • Prazo para envio: [2017-08-13 Dom 23:59]
        • Gabarito: exercicio1-gabarito.v
  2. [2017-08-11 Sex 12:00]–[2017-08-11 Sex 13:50] O isomorfismo de Curry-Howard ✓
  3. [2017-08-14 Seg 12:00]–[2017-08-14 Seg 13:50] O isomorfismo de Curry-Howard (cont.) ✓
    • Exercícios:
      • Arquivo coq: exercicio2.v
        • A solução dos exercícios deve ser enviada para contato@flaviomoura.mat.br
        • Assunto do email: [pftt] Exercício 2
        • Prazo para envio: [2017-08-20 Dom 23:59]
        • Gabarito: exercicio2-gabarito.v
  4. [2017-08-18 Sex 12:00]–[2017-08-18 Sex 13:50] O isomorfismo de Curry-Howard (cont.) ✓
    • Rascunho da aula (com exercícios!): aula4.v
  5. [2017-08-21 Seg 12:00]–[2017-08-21 Seg 13:50]
    • O arquivo com as notas de aula foi atualizado (pdf)
    • Arquivo coq: naturais20172.v
      • A solução dos exercícios deve ser enviada para contato@flaviomoura.mat.br
      • Assunto do email: [pftt] naturais20172
      • Prazo para envio: [2017-08-27 Dom 23:59]
      • Gabarito: naturais20172gabarito.v
  6. [2017-08-25 Sex 12:00]–[2017-08-25 Sex 13:50] Resolução de exercícios ✓
  7. [2017-08-28 Seg 12:00]–[2017-08-28 Seg 13:50] Formalização de listas e algumas propriedades ✓
    • Arquivo coq: listas20172.v
      • A solução dos exercícios deve ser enviada para contato@flaviomoura.mat.br
      • Assunto do email: [pftt] listas20172
      • Prazo para envio: [2017-09-08 Sex 23:59]
      • Gabarito:
  8. [2017-09-01 Sex 12:00]–[2017-09-01 Sex 13:50] Exercícios ✓
  9. [2017-09-04 Seg 12:00]–[2017-09-04 Seg 13:50] Exercícios ✓
  10. [2017-09-08 Sex 12:00]–[2017-09-08 Sex 13:50] Algoritmos de ordenação ✓
    • Arquivo da aula de hoje: insertionsort20172.v
    • Arquivo coq: algoritmo20172.v
      • A solução dos exercícios deve ser enviada para contato@flaviomoura.mat.br
      • Assunto do email: [pftt] algoritmo20172
      • Prazo para envio: [2017-10-08 Dom 23:59]
  11. [2017-09-11 Seg 12:00]–[2017-09-11 Seg 13:50] Funções recursivas ✓
    • Sugestões de algoritmos a serem formalizados:
      • Selection sort
      • Bubble sort
  12. [2017-09-15 Sex 12:00]–[2017-09-15 Sex 13:50] Princípios indutivos ✓
    • Baixe o arquivo https://softwarefoundations.cis.upenn.edu/lf-current/lf.tgz
      • Após descompactar o arquivo lf.tgz, abra um terminal e entre no diretório lf.
      • Em seguida, execute o comando 'make'. Isto fará co que vários arquivos '.vo' sejam gerados.
      • Abra o arquivo IndPrinciples.v, leia o texto e resolva os exercícios propostos.
      • Envie o arquivo resolvido para contato@flaviomoura.mat.br
      • Assunto do email: [pftt] IndPrinciples
      • Prazo para envio: [2017-09-22 Sex 23:59]
  13. [2017-09-18 Seg 12:00]–[2017-09-18 Seg 13:50] Princípios indutivos (cont.) ✓

    [2017-09-22 Sex 12:00]–[2017-09-22 Sex 13:50] Não haverá aula

    [2017-09-25 Seg 12:00]–[2017-09-25 Seg 13:50] ITP, FroCoS and Tableaux conferences

    [2017-09-29 Sex 12:00]–[2017-09-29 Sex 13:50] ITP, FroCoS and Tableaux conferences

  14. [2017-10-02 Seg 12:00]–[2017-10-02 Seg 13:50] Numerais de Church ✓
    • Arquivo coq: church.v
      • A solução dos exercícios deve ser enviada para contato@flaviomoura.mat.br
      • Assunto do email: [pftt] church
      • Prazo para envio: [2017-10-15 Dom 23:59]
  15. [2017-10-06 Sex 12:00]–[2017-10-06 Sex 13:50] Funções recursivas no cálculo λ ✓
  16. [2017-10-09 Seg 12:00]–[2017-10-09 Seg 13:50] Observações sobre a formalização do Bubble Sort ✓
    • Exercício sugerido: refazer a prova do lema bubble\_equiv usando o fato que equiv é uma relação transitiva.
      • Os lemas a serem provados são equiv_sub, equiv_trans e bubble_equiv'.
      • Arquivo: bubbleSortequiv.v
  17. [2017-10-13 Sex 12:00]–[2017-10-13 Sex 13:50] Formalização do Bubble Sort ✓
    • Arquivo coq: bubbleSort2017-2.v
      • A solução dos exercícios deve ser enviada para contato@flaviomoura.mat.br
      • Assunto do email: [pftt] bubbleSort2017-2
      • Prazo para envio: [2017-10-22 Dom 23:59]
  18. [2017-10-16 Seg 12:00]–[2017-10-16 Seg 13:50] Selection Sort
    • Arquivo coq: selectionSort.v
      • A solução dos exercícios deve ser enviada para contato@flaviomoura.mat.br
      • Assunto do email: [pftt] bubbleSort2017-2
      • Prazo para envio: [2017-10-29 Dom 23:59]
  19. [2017-10-20 Sex 12:00]–[2017-10-20 Sex 13:50]

    [2017-10-23 Seg 12:00]–[2017-10-23 Seg 13:50] Semana Universitária

    [2017-10-27 Sex 12:00]–[2017-10-27 Sex 13:50] Semana Universitária

  20. [2017-10-30 Seg 12:00]–[2017-10-30 Seg 13:50]
  21. [2017-11-03 Sex 12:00]–[2017-11-03 Sex 13:50]
  22. [2017-11-06 Seg 12:00]–[2017-11-06 Seg 13:50]
  23. [2017-11-10 Sex 12:00]–[2017-11-10 Sex 13:50]
  24. [2017-11-13 Seg 12:00]–[2017-11-13 Seg 13:50]
  25. [2017-11-17 Sex 12:00]–[2017-11-17 Sex 13:50]
  26. [2017-11-20 Seg 12:00]–[2017-11-20 Seg 13:50]
  27. [2017-11-24 Sex 12:00]–[2017-11-24 Sex 13:50]
  28. [2017-11-27 Seg 12:00]–[2017-11-27 Seg 13:50]
  29. [2017-12-01 Sex 12:00]–[2017-12-01 Sex 13:50]

Author: Flávio Leonardo Cavalcanti de Moura

Created: 2017-10-16 Seg 13:56

Validate