PhD Course on “Introduzione a CoQ”
- Period
- 9-17 settembre 2020
Series to which this belongs
- 33° ciclo
- 34° ciclo
- 35° ciclo
Description
Coq (basato sul Calcolo delle Costruzioni Induttive) è un sistema complesso, pensato per un utilizzo professionale (non è un toy-tool), ed il suo uso richiede una curva di apprendimento graduale e non banale.
Lo scopo di questo corso è di introdurre le basi teoriche e pratiche di CoQ ed è indirizzato a tutte le persone interessate al ragionamento meccanico assistito (indipendentemente dall’area di ricerca).
CoQ è utilizzato con successo nelle seguenti aree:
- specifica e dimostrazione di proprietà di programmi;
- specifica e dimostrazione di proprietà di protocolli di rete;
- basi di dati relazionali;
- verifica e specifica di sistemi HW;
- implementazione di sistemi logici;
- meccanizzazione della matematica (da quella continua a quella discreta).
Il corso, per chi sarà interessato, prevederà un piccolo progetto implementativo finale.
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
Attachments
- Documents
-