CdSINFORMATICA
Codice648AA
CFU6
PeriodoSecondo semestre
LinguaInglese
| Moduli | Settore/i | Tipo | Ore | Docente/i | |
| FOUNDATION OF COMPUTING | INF/01 | LEZIONI | 48 |
|
Lo scopo del corso è quello di introdurre tecniche per la specifica di sistemi concorrenti e distribuiti, con particolare enfasi sui formalismi algebrici e categoriali.
The aim of the course is to introduce techniques for the specification of concurrent and distributed systems, with particular emphasis on algebraic and categorical formalisms.
L'esame consiste in un seminario (ed eventualmente una prova orale) su un argomento avanzato presentato durante il corso. Il seminario ha l'obbiettivo di verificare la capacità dello studente nell'affrontare temi allo stato dell'arte riguardo l'uso di metodi formali per la specifica di sistemi. L'eventuale prova orale ha l'obiettivo di accertare che lo studente abbia acquisito sufficiente familiarità con i concetti di base legati alle tecniche algebriche di specifica.
The examination consists of a seminar (and possibly an oral test) on an advanced topic presented during the course. The seminar is aimed at testing the student's ability to deal with state-of-the-art topics concerning the use of formal methods for the specification of systems. The objective of the oral examination, if any, is to ascertain that the student has acquired sufficient familiarity with the basic concepts of algebraic specification techniques.
Al termine del corso lo studente sarà in grado di utilizzare tecniche algebriche allo stato dell'arte per quel che riguarda la specifica di sistemi concorrenti e distribuiti.
At the end of the course, the student will be able to use state-of-the-art algebraic techniques for the specification of concurrent and distributed systems.
Tutte le lezioni hanno una struttura seminariale e alcune sono dedicate alla soluzione guidata di problemi al fine di far meglio comprendere le potenzialità espressive dei tool algebrici per la specifica introdotti nel corso.
All lectures have a seminar structure and some are dedicated to guided problem-solving in order to better understand the expressive potential of the algebraic tools for specification introduced in the course.
Al termine del corso lo studente avrà acquisito maggiore consapevolezza sull'importanza di descrivere formalmente le proprietà desiderate di un sistema e posto in contesto alcune delle tecniche algebriche attualmente utilizzate per quel che riguarda la specifica di dette proprietà.
By the end of the course, the student will have become more aware of the importance of formally describing the desired properties of a system and put into context some of the algebraic techniques currently used in specifying these properties.
La struttura seminariale, che include un momento specifico per l'interazione con gli studenti, e le esercitazioni permettono di verificare la sensibilità del gruppo rispetto alla rilevanza dei temi trattati durante il corso, mentre la prova seminariale consente di evidenziare la capacità del singolo nell'inquadramento generale dello specifico argomento trattato.
The seminar structure, which includes a specific time for interaction with the students, and the exercises allow the group's sensitivity to the relevance of the topics covered during the course to be tested, while the seminar paper allows the individual's ability to be tested in the general framing of the specific topic covered.
Conoscenze di base di logica proposizionale e algebra.
Basic knowledge of propositional logic and algebra.
Il corso si basa su lezioni frontali di tipo seminariale e presentazione di problemi in sessioni di q&a.
The course is based on seminar-style lectures and presentation of problems in Q & A sessions.
Fondamenti categoriali
- Introduzione alla teoria delle categorie
- Monadi, categorie monoidali, calcoli grafici
- Categorie arricchite, semantiche funtoriali
Sistemi di riscrittura
- Calcolo delle relazioni
- Riscrittura astratta e basata su sintassi
- Riscrittura parallele e annidata
- Confluenza e terminazione
Semantiche osservazionali
- Bisimulazioni probabilistiche
- Sistemi di transizione e coalgebre
- Leggi distributive
Analisi statica di sistemi
- Intepretazione astratta
- Sistemi di tipi e semantica denotazionale
Logiche
- Logiche modali quantificate
- Corrispondenza di Curry-Howard
- Modelli in stile "dialectica"
Categorical Foundations
- Introduction to category theory
- Monads, monoidal categories, graphical calculations
- Enriched categories, functorial semantics
Rewriting systems
- Calculus of relations
- Abstract and syntax-based rewriting
- Parallel and nested rewriting
- Confluence and termination
Observational semantics
- Probabilistic bisimulations
- Transition systems and coalgebras
- Distributional laws
Static systems analysis
- Abstract interpretation
- Type systems and denotational semantics
Logics
- Quantified modal logics
- Curry-Howard correspondence
- Dialectica models
Andrew M. Pitts, Categorical Logic. In Samson Abramsky, Dov M. Gabbay and Thomas S. E. Maibaum (eds.), Handbook of Logic in Computer Science, Volume 5. Oxford University Press, 2000.
Richard Bird and Oege de Moor, The algebra of programming. Prentice Hall, 1997.
Patrick Cousot, Principles of abstract interpretation. The MIT Press, 2021.
Benjamin C. Pierce, Basic category theory for computer scientists. The MIT Press, 1991.
Davide Sangiorgi, Introduction to bisimulation and coinduction. Cambridge University Press, 2011.
Seminario su uno degli argomenti avanzati discussi durante il corso ed eventuale prova orale.
Seminar on one of the advanced topics discussed during the course and possible oral test.