30214 - FONDAMENTI LOGICI DELL'INFORMATICA

Conoscenze e abilità da conseguire

Al termine del corso lo studente ha acquisito le basi logico formali di aree dell'informatica teorica quali il lambda-calcolo, i sistemi di riscrittura, la teoria delle basi di dati e i metodi formali volti all’analisi e alla verifica di programmi. E' in grado di codificare in lambda-calcolo vari costrutti di programmazione, di esprimere interrogazioni a basi di dati in forma predicativa, di specificare proprietà di sistemi reattivi come formule di logiche temporali e di descrivere protocolli di comunicazione come formule di logiche substrutturali.

Contenuti

Primo modulo:

1. Richiami di Logica Proposizionale e al Prim'Ordine.
Sintassi, Semantica, Correttezza e Completezza, Indecidibilità della
Logica al Prim'Ordine

2. Lambda Calcolo non tipato.
Sintassi e Semantica Operazionale. Il Lambda Calcolo come linguaggio di
programmazione: stategie di valutazione e rappresentazione dei dati;
Turing completezza (cenni).

3. Meta-teoria del Lambda Calcolo non tipato.
Confluenza.

4. Lambda Calcolo Tipato Semplice e Isomorfismo di Curry-Howard
Sintassi alla Curry e alla Church. Isomorfismo con la logica
proposizionale minimale. Algoritmi per il type-checking e la type-
inference.

5. Meta-teoria del Lambda Calcolo tipato semplice.
Teoremi di normalizzazione debole e forte.

6. Isomorfismo di Curry-Howard ed estensioni del sistema di tipi.
Tipi prodotto, coprodotto, vuoto e singleton. Polimorfismo parametrico
(cenni al System F). Cenni ai sistemi di tipi dipendenti e al tipaggio
alla Hindley-Milner.

Secondo modulo:

1. Modellazione e analisi statica di sistemi distribuiti
Sintassi e semantica operazionale del pi-calcolo; Logica lineare;
Logica lineare come sistema di tipi per il pi-calcolo; meta-teoria
del pi-calcolo tipato

2. Logica e Metodi Formali
LTL e CTL: sintassi e semantica. Sistemi Reattivi e Loro Verifica.
Model Checking.

Testi/Bibliografia

Per il primo modulo:

- H.P. Barendregt: The Lambda Calculus, Its Syntax and Semantics (Studies in Logic and the Foundations of Mathematics, Volume 103).

- J.Y. Girard, Y. Lafont, P. Taylor: Proof and Types. Available on-line at http://www.paultaylor.eu/stable/Proofs+Types.html

Congiuntamente i due testi coprono tutti gli argomenti visti a lezione.

Per il secondo modulo: 

- E. Clarke and O. Grumberg and D. Peled. Model Checking. MIT Press, 1999.

Il testo copre i soli argomenti relativi a "Logica e Metodi Formali".
Per quanto riguarda "Modellazione e analisi statica di sistemi distribuiti" il docente fornirà materiale didattico integrativo.

Metodi didattici

Il corso si svolge al primo semestre e prevede in lezioni frontali in aula.

Durante le lezioni frontali vengono trattati esaustivamente tutti gli argomenti del corso, fornendo esempi per le definizioni date e dimostrazioni dettagliate della maggior parte dei teoremi.

A seconda dell'argomento trattato o si utilizzeranno lucidi messi precedentemente a disposizione oppure il docente scriverà interattivamente i lucidi su un tablet e li fornirà a fine lezione agli studenti. La seconda modalità è più indicata nel caso di dimostrazioni di una certa complessità perchè permette al docente di adattare dinamicamente la dimostrazione al livello di conoscenze degli studenti e di procedere più lentamente nella spiegazione.

Modalità di verifica e valutazione dell'apprendimento

L'esame è unico per entrambi i moduli e consiste in una prova orale. La prova orale verte su tutti gli argomenti visti a lezione. Per ogni modulo vengono poste dal docente del modulo domande per circa 10 minuti. Le domande sono finalizzate a verificare l'effettiva comprensione sia degli argomenti esposti, che della loro rilevanza. Sarà valutata l'accuratezza delle risposte e delle definizioni, la chiarezza e la sintesi con cui si espongono gli argomenti e la capacità di collegamento dei diversi argomenti trattati. Il voto da verbalizzare viene concordato fra i due docenti al termine delle domande. La verbalizzazione avviene seduta stante, a meno del caso in cui lo studente sia indeciso sulla verbalizzazione del voto. In tal caso la decisione deve essere presa entro le 24 ore successive.

Persone con disabilità e DSA

Le persone con disabilità o disturbi specifici dell’apprendimento hanno diritto a speciali adattamenti in relazione alla loro condizione, previa valutazione del Servizio d’ateneo per le studentesse e gli studenti con disabilità e DSA. Si prega di non rivolgersi al/la docente, ma di contattare il Servizio per un appuntamento. Sarà cura del Servizio stabilire quali adattamenti si rendono opportuni. Maggiori informazioni alla pagina https://site.unibo.it/studenti-con-disabilita-e-dsa/it/per-studenti.

Strumenti a supporto della didattica

Verranno forniti i lucidi presentati o scritti interattivamente a lezione. Si daranno inoltre puntatori ad articoli scientifici e testi divulgativi scaricabili liberamente dal Web.

Orario di ricevimento

Consulta il sito web di Claudio Sacerdoti Coen

Consulta il sito web di Luca Padovani