Dottorato in Informatica

Introduzione a CoQ

Periodo
3-11 SETTEMBRE 2019

Docenti
Andrea Masini

Cicli in cui è offerta

32° Ciclo
33° ciclo
34° ciclo

Descrizione

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.
 

Allegati

Documenti