Mini-Corso su CoQ

June 28, 2020

Settembre 2020.
Gli orari del corso (4 lezioni di 3 ore ciascuna) verranno comunicati in seguito.

CoQ
Andrea Masini (Università di Verona)

Programma
1) Richiami di deduzione naturale (classica ed intuizionista) e di lambda calcolo tipato.
2) Esempi di semplici dimostrazioni in CoQ (Goal, Assunzioni e Tattiche).
3) Programmazione funzionale in CoQ.
4) Tipi di dato strutturati.
5) Polimorfismo e funzioni di ordine superiore.
6) Le tattiche di base.
7) Logica in CoQ.
8) Induzione