PCC116 - Lógica aplicada à computação

Repositório contendo o material da disciplina PCC116 para o semestre 2021/2.

Conteúdo da disciplina.

• Semana 01

  • Aula 01 - 24/08/2021 - Apresentação da disciplina

  • Aula 02 - 26/08/2021 - Revisão: Programação Funcional

• Semana 02

  • Aula 03 - 31/08/2021 - Lógica proposicional - Parte 01

  • Aula 04 - 02/09/2021 - Lógica proposicional - Parte 02

• Semana 03

  • Aula 05 - 07/09/2021 - Lambda cálculo não tipado

  • Aula 06 - 09/09/2021 - Lambda cálculo tipado simples

• Semana 04

  • Aula 07 - 14/09/2021 - Sistema de Hindley-Milner

  • Aula 08 - 16/09/2021 - Sistema F

• Semana 05

  • Aula 09 - 21/09/2021 - Lógica de Predicados

  • Aula 10 - 23/09/2021 - Introdução à linguagem Agda

• Semana 06

  • Aula 11 - 28/09/2021 - Números naturais em Agda

  • Aula 12 - 30/09/2021 - Relações em Agda

• Semana 07

  • Aula 13 - 05/10/2021 - Lógica em Agda

  • Aula 14 - 07/10/2021 - Evidências em Agda

• Semana 08

  • Aula 15 - 12/10/2021 - Listas e funções de ordem superior em Agda

  • Aula 16 - 14/10/2021 - Estudo de caso: Formalizando o insertion sort

• Semana 09

  • Aula 17 - 19/10/2021 - Programação com tipos dependentes - Parte I

  • Aula 18 - 21/10/2021 - Programação com tipos dependentes - Parte II

• Semana 10

  • Aula 19 - 26/10/2021 - Recursão geral em Agda
  • Aula 20 - 28/10/2021 - Co-indução em Agda

• Semana 11

  • Aula 21 - 02/11/2021 - Formalizando expressões aritméticas tipadas
  • Aula 22 - 04/11/2021 - Formalizando o lambda-cálculo não tipado e tipado simples

• Semana 12

  • Aula 23 - 09/11/2021 - Interpretando a linguagem IMP
  • Aula 24 - 11/11/2021 - Programação genérica

• Semana 13

  • Aula 25 - 16/11/2021 - Reflection em Agda
  • Aula 26 - 18/11/2021 - Martin-Löf Type Theory

• Semana 14

  • Aula 27 - 30/11/2021 - Introdução à Homotopy Type Theory
  • Aula 28 - 02/12/2021 - Introdução ao Cubical Agda

Listas de exercícios

• Lista 01 - Lógica proposicional

  • Data para entrega: 10/09/2021, pela plataforma Moodle.
  • Link para a lista: https://github.com/rodrigogribeiro/pcc116-2021-2/blob/master/listas/lista01/lista01.pdf

• Lista 02 - Lambda-cálculo

  • Data para entrega: 17/09/2021, pela plataforma Moodle.
  • Link para a lista: https://github.com/rodrigogribeiro/pcc116-2021-2/blob/master/listas/lista02/lista02.pdf

• Lista 03 - Inferência de tipos e Sistema F

  • Data para entrega: 02/10/2021, pela plataforma Moodle.
  • Link para a lista: https://github.com/rodrigogribeiro/pcc116-2021-2/blob/master/listas/lista03/lista03.pdf

• Lista 04 - Definições e teoremas sobre booleanos

  • Data para entrega: 09/10/2021, pela plataforma Moodle.
  • Formato de entrega: arquivo .zip contendo todo o código da biblioteca pcc116-agda-lib.
  • Arquivos contendo os exercícios da lista:
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/Bool/Bool.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/Bool/BoolTheorems.agda

• Lista 05 - Definições e teoremas sobre números naturais.

  • Data para entrega: 16/10/2021, pela plataforma Moodle.
  • Formato de entrega: arquivo .zip contendo todo o código da biblioteca pcc116-agda-lib.
  • Arquivos contendo os exercícios da lista:
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/Nat/Le.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/Nat/LeAlt.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/Nat/NatTheorems.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/Nat/EvenOdd.agda

• Lista 06 - Lógica em Agda, Evidências.

  • Data para entrega: 23/10/2021
  • Formato de entrega: arquivo .zip contendo todo o código da biblioteca pcc116-agda-lib.
  • Arquivos contendo os exercícios da lista:
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/Product/ProductTheoerms.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/Sum/SumTheorems.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/Biconditional/BiconditionalTheorems.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Relation/Decidable/Dec.agda

• Lista 07 - Listas e funções de ordem superior.

  • Data para entrega: 30/10/2021
  • Formato de entrega: arquivo .zip contendo todo o código da biblioteca pcc116-agda-lib.
  • Arquivos contendo os exercícios da lista:
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/List/ListTheorems.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/List/Relation/All.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/List/Relation/Any.agda

• Lista 08 - Programação com tipos dependentes - Parte I.

  • Data para entrega: 06/11/2021
  • Formato de entrega: arquivo .zip contendo todo o código da biblioteca pcc116-agda-lib.
  • Arquivos contendo os exercícios da lista:
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/Vec/Vec.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/Vec/Matrix.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Language/Data/Data.agda

• Lista 09 - Programação com tipos dependentes - Parte II.

  • Data para entrega: 13/11/2021
  • Formato de entrega: arquivo .zip contendo todo o código da biblioteca pcc116-agda-lib.
  • Arquivos contendo os exercícios da lista:
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/List/Relation/Sublist.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/List/Sorting/Extrinsic/StalinSort.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/List/Sorting/Extrinsic/StalinSortTheorems.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/List/Sorting/Intrinsic/InsertionSort.agda

• Lista 10 - Recursão não estrutural.

  • Data para entrega: 20/11/2021
  • Formato de entrega: arquivo .zip contendo todo o código da biblioteca pcc116-agda-lib.
  • Arquivos contendo os exercícios da lista:
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/Nat/Div/DivIntrinsic.agda

• Lista 11 - Noções de semântica formal.

  • Data para entrega: 27/11/2021
  • Formato para entrega: arquivo .zip contendo todo o código da biblioteca pcc116-agda-lib.
  • Arquivos contendo os exercícios da lista:
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Language/Exp/Intrinsic.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Language/Exp/Extrinsic.agda

• Lista 12 - Programação genérica.

  • Data para entrega: 04/12/2021
  • Formato para entrega: arquivo .zip contendo todo o código da biblioteca pcc116-agda-lib
  • Arquivo contendo os exercícios da lista:
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/Generic/GSize.agda

• Lista 13 - Introdução à Teoria de tipos de Martin-Löf

  • Data para entrega: 11/12/2021
  • Formato para entrega: arquivo .zip contendo todo o código da biblioteca pcc116-agda-lib
  • Arquivo contendo os exercícios da lista:
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/MLTT/Spartan.agda

• Lista 14 - Cubical Agda

  • Data para entrega: 18/12/2021
  • Formato para entrega: arquivo .zip contendo todo o código da biblioteca pcc116-agda-lib
  • Arquivo contendo os exercícios da lista:
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/CTT/Silly.agda

Código de exemplo

• Implementação de proof search usando cálculo de sequentes

• Interpretador para o lambda-cálculo não tipado

• Interpretador para o lambda-cálculo não tipado com índices De Bruijn

• Inferência de tipos para o lambda-cálculo tipado simples

• Interpretador do Sistem F

Biblioteca Agda

Parte do conteúdo da disciplina envolverá o desenvolvimento de uma biblioteca Agda. A biblioteca pode ser encontrada no seguinte link:

https://github.com/rodrigogribeiro/pcc116-agda-lib