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