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

Table of Contents

1 Quadro de Avisos

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

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

1.3 Apresentação da disciplina (pdf)

2 Quadro de notas:

Matrícula Faltas(*) Faltas (%) Menção
100109829 3 10.71 SR
110146123 7 25.00 MS
120049031 16 57.14 SR
120050943 2 7.14 SS
120126443 6 21.43 MM
140153641 4 14.29 MM
140160299 4 14.29 SS
150014961 6 21.43 MS
150021623 4 14.29 SS
150023928 14 50.00 SR
150126689 5 17.86 SS
150143290 4 14.29 TR
150143362 7 25.00 MM
160003318 5 17.86 TR
170043339 12 42.86 TR

(*) Última atualização: [2017-11-27 Mon 14:43]

3 Calendário de aulas:

  1. [2017-08-07 Mon 12:00]–[2017-08-07 Mon 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 Sun 23:59]
        • Gabarito: exercicio1-gabarito.v
  2. [2017-08-11 Fri 12:00]–[2017-08-11 Fri 13:50] O isomorfismo de Curry-Howard ✓
  3. [2017-08-14 Mon 12:00]–[2017-08-14 Mon 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 Sun 23:59]
        • Gabarito: exercicio2-gabarito.v
  4. [2017-08-18 Fri 12:00]–[2017-08-18 Fri 13:50] O isomorfismo de Curry-Howard (cont.) ✓
    • Rascunho da aula (com exercícios!): aula4.v
  5. [2017-08-21 Mon 12:00]–[2017-08-21 Mon 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 Sun 23:59]
      • Gabarito: naturais20172gabarito.v
  6. [2017-08-25 Fri 12:00]–[2017-08-25 Fri 13:50] Resolução de exercícios ✓
  7. [2017-08-28 Mon 12:00]–[2017-08-28 Mon 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 Fri 23:59]
      • Gabarito: listas20172gabarito.v
  8. [2017-09-01 Fri 12:00]–[2017-09-01 Fri 13:50] Exercícios ✓
  9. [2017-09-04 Mon 12:00]–[2017-09-04 Mon 13:50] Exercícios ✓
  10. [2017-09-08 Fri 12:00]–[2017-09-08 Fri 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 Sun 23:59]
  11. [2017-09-11 Mon 12:00]–[2017-09-11 Mon 13:50] Funções recursivas ✓
    • Sugestões de algoritmos a serem formalizados:
      • Selection sort
      • Bubble sort
  12. [2017-09-15 Fri 12:00]–[2017-09-15 Fri 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 Fri 23:59]
  13. [2017-09-18 Mon 12:00]–[2017-09-18 Mon 13:50] Princípios indutivos (cont.) ✓

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

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

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

  14. [2017-10-02 Mon 12:00]–[2017-10-02 Mon 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 Sun 23:59]
      • Gabarito: churchgabarito.v
  15. [2017-10-06 Fri 12:00]–[2017-10-06 Fri 13:50] Funções recursivas no cálculo λ ✓
  16. [2017-10-09 Mon 12:00]–[2017-10-09 Mon 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 Fri 12:00]–[2017-10-13 Fri 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 Sun 23:59]
      • Gabarito: bubbleSort20172gabarito.v
  18. [2017-10-16 Mon 12:00]–[2017-10-16 Mon 13:50] Selection Sort ✓
  19. [2017-10-20 Fri 12:00]–[2017-10-20 Fri 13:50] Selection Sort ✓

    [2017-10-23 Mon 12:00]–[2017-10-23 Mon 13:50] Semana Universitária (Não haverá aula)

    [2017-10-27 Fri 12:00]–[2017-10-27 Fri 13:50] Semana Universitária (Não haverá aula)

  20. [2017-10-30 Mon 12:00]–[2017-10-30 Mon 13:50] Selection Sort ✓
  21. [2017-11-03 Fri 12:00]–[2017-11-03 Fri 13:50] Selection Sort ✓
  22. [2017-11-06 Mon 12:00]–[2017-11-06 Mon 13:50] Selection Sort ✓
  23. [2017-11-10 Fri 12:00]–[2017-11-10 Fri 13:50] Selection Sort ✓
  24. [2017-11-13 Mon 12:00]–[2017-11-13 Mon 13:50] Selection Sort ✓
    • Arquivo coq: selectionSort20172sorts.v
    • A solução dos exercícios deve ser enviada para contato@flaviomoura.mat.br
    • Assunto do email: [pftt] selectionSort20172sorts
    • Prazo para envio: [2017-11-26 Sun 23:59]
    • Gabarito:
  25. [2017-11-17 Fri 12:00]–[2017-11-17 Fri 13:50] Confluência do cálculo lambda sem tipos
    • Arquivo coq: ulc-20172.v
    • A solução dos exercícios deve ser enviada para contato@flaviomoura.mat.br
    • Assunto do email: [pftt] ulc-20172
    • Prazo para envio: [2017-11-26 Sun 23:59]
    • Gabarito:
  26. [2017-11-20 Mon 12:00]–[2017-11-20 Mon 13:50] Os inteiros em Coq ✓
    • Complete a definição da função recursiva div_bin que implementa o algoritmo da divisão de Euclides para inteiros positivos:

      Require Import ZArith.
      
       div_bin (n m: positive) : Z*Z := 
       match n with 
       | 1%positive => match m with
                       | 1%positive => (1,0)
                       | _ => (0,1)
                       end.
       | xO n' => ... (Zpos m) ...
       | xI n' => ... (Zpos m) ...
       end
      
  27. [2017-11-24 Fri 12:00]–[2017-11-24 Fri 13:50]
  28. [2017-11-27 Mon 12:00]–[2017-11-27 Mon 13:50]
  29. [2017-12-01 Fri 12:00]–[2017-12-01 Fri 13:50]

Author: Flávio Leonardo Cavalcanti de Moura

Created: 2017-11-27 Mon 15:11

Validate