Introduzione a CoQ
- Period
- 3-11 SETTEMBRE 2019
- Academic staff
-
Andrea Masini
Series to which this belongs
- 32° Ciclo
- 33° ciclo
- 34° ciclo
Description
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.
Attachments
- Documents
-
