Sito web di Coq

Sito web del mini corso http://www-sop.inria.fr/members/Enrico.Tassi/padova2017/

Pagina di prova

Coq può funzionare dentro il browser (navigatore).

attendi che la pagina si carichi, un pannello si apre sulla destra
verifica con Coq ogni linea del documento premendo ALT-N (le frasi accettate da Coq diventano grigio chiaro).
torna indietro con ALT-P
OK, tutto funziona!

Introduzione

Coq: un assistente alla dimostrazione

Cos'è un assistente alla dimostrazione?!
Coq è basato sulla (una variante) della teoria dei tipi di Martin Löf
Coq è utilizzato per
- formalizzare matematica
- verificare software

Chi sono io?

Enrico Tassi
Sviluppatore Coq
Ricercatore (implementazione PA e loro utilizzo)

Obiettivi del mini corso

Vedere una applicazione pratica della teoria dei tipi
Introduzione a un assistente alla dimostrazione (proof assistant, interactive theorem prover)

Lezioni

lezione 1: Coq: un linguaggio di programmazione funzionale
lezione 2: Curry Howard: la logica di Coq e le prime dimostrazioni
lezione 3: Induzione: proprietà di programmi ricorsivi
lezione 4: Riflessione computazionale: l'esecuzione di un programma è una prova

Iniziamo!

Prima lezione: Coq: un linguaggio di programmazione funzionale