Didactic Finucular

Repositório para conter links interessantes sobre teoria de tipos, lógica e assistente de provas

Cursos

• Assistants de preuves. Curso sobre assistente de provas, teoria e prática em Coq, ministrado por Bruno Barras e Matthieu Sozeau. Página principal em francês, mas os slides parecem ser todos em inglês. (Arquivo*) TODO: Arquivar pdfs.

• Computational logic: from Artificial intelligence to Zero bugs. The goal of this course is to explain how logic can be used in order for modeling problems of computational or mathematical nature, and how computers can be used to achieve this. In particular, we will present proof assistants, which allow to formalize human reasoning by interactively constructing proofs, and explain their use to certify the absence of bugs in programs. Arquivo Notas: Utiliza o excelentíssimo livro Program = Proof de Samuel Mimram.

Livros

• Logic and Proof. A textbook that is a first rigorous proving course that teaches Lean at the same time. (Arquivo) TODO: Verificar arquivamento.

• Program = Proof. These are the extended notes for the INF551 course which I (Samuel) taught at École Polytechnique starting from 2019. The goal is to give a first introduction to the Curry-Howard correspondence between programs and proofs, from a theoretical programmer’s perspective: we want to understand the theory behind logic and programming languages, but also to write concrete programs (in OCaml) and proofs (in Agda). Although most of the material is self-contained, the reader is supposed to be already acquainted with logic and programming. Arquivo

Porque do nome?

Foi uma sugestão do GitHub...