View syllabus
FOUNDATION OF COMPUTING
FABIO GADDUCCI
Academic year2022/23
CourseCOMPUTER SCIENCE
Code648AA
Credits6
PeriodSemester 2
LanguageEnglish

ModulesAreaTypeHoursTeacher(s)
FOUNDATION OF COMPUTINGINF/01LEZIONI48
FABIO GADDUCCI unimap
Obiettivi di apprendimento
Learning outcomes
Conoscenze

Lo scopo del corso è quello di introdurre tecniche per la specifica di sistemi concorrenti e distribuiti, con particolare enfasi sui formalismi algebrici e categoriali.

Knowledge

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.

Modalità di verifica delle conoscenze

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.

Assessment criteria of knowledge

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.

Capacità

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.

Skills

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.

Modalità di verifica delle capacità

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.

Assessment criteria of skills

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.

Comportamenti

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à.

Behaviors

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.

Modalità di verifica dei comportamenti

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.

 

Assessment criteria of behaviors

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.

Prerequisiti (conoscenze iniziali)

Conoscenze di base di logica proposizionale e algebra.

Prerequisites

Basic knowledge of propositional logic and algebra.

Indicazioni metodologiche

Il corso si basa su lezioni frontali di tipo seminariale e presentazione di problemi in sessioni di q&a.

Teaching methods

The course is based on seminar-style lectures and presentation of problems in Q & A sessions.

Programma (contenuti dell'insegnamento)

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"
Syllabus

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
Bibliografia e materiale didattico

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.

Modalità d'esame

Seminario su uno degli argomenti avanzati discussi durante il corso ed eventuale prova orale.

 

Assessment methods

Seminar on one of the advanced topics discussed during the course and possible oral test.

Updated: 19/06/2023 14:19