PhD in Computer Science

Introduzione a CoQ

Period
3-11 SETTEMBRE 2019

Academic staff
Andrea Masini

Series to which this belongs

32° Ciclo
33° ciclo
34° ciclo

Description

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.
 

Attachments

Documents