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) Funzioni parziali e totali
9) Isomorfismo di Curry-Howard
10)Induzione e cieli di co-induzione.
Prerequisiti: nozioni di base di logica (ad esempio i contenuti del corso di logica della laurea triennale in Informatica di Verona,
http://www.di.univr.it/?ent=oi&aa=2018%2F2019&codiceCs=S24&codins=11098&cs=420&discr=Matricole+pari&discrCd=&lang=en
Esame: implementazione di sistemi logici e computazionali in CoQ.