Instalação

• Acesse o site https://coq.inria.fr e faça o download para seu sistema operacional.

• É importante a escolha de um IDE para uso da ferramenta. Existem duas opções, que são bem similares:

  1. CoqIDE que é instalado em conjunto com Coq em algumas distribuições binárias.
  2. Proof-general que é um plug-in para o editor emacs.

Pré-requisitos

De maneira geral espera-se que os alunos tenham noções de lógica formal (dedução natural para lógica clássica) e programação funcional. Conhecimento básico de semântica operacional é útil, porém não obrigatório.

Materiais para o curso

O código fonte a ser utilizado durante todo o curso está disponível neste link.