PhD in Computer Science

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
  • pdf   Flyer   (pdf, it, 172 KB, 11/09/20)