3. Aula 3: Programas e Teoremas🔗

Esta aula passa de provar a programar, seguindo o capítulo 2 do Hitchhiker's Guide to Logical Verification.A. Baanen, A. Bentkamp, J. Blanchette, J. Hölzl, J. Limperg, The Hitchhiker's Guide to Logical Verification, edição de 2026, capítulo 2. Ela apresenta tipos indutivos, definições de funções por casamento de padrões e recursão, avaliação e o enunciado de teoremas sobre programas, sem realizar prova alguma ainda.

Esta aula também está disponível como slides de apresentação.

1. 3.1. Das Provas aos Programas
2. 3.2. Tipos Indutivos
3. 3.3. Funções por Casamento de Padrões e Recursão
4. 3.4. Polimorfismo e Argumentos Implícitos
5. 3.5. Avaliação
6. 3.6. Enunciados de Teoremas
7. 3.7. Exemplos Resolvidos
8. 3.8. Exercícios