FOC - Foundation of Computing

Docente

Ugo Montanari

Orario Lezioni/Timetable Anno Accademico 2021-2022

Martedì 11:00-12:45 Aula Fib X1

Mercoledì 11:00-12:45 Aula  Fib X1

Link di Meet:  Google Classroom/Meet

Prima Lezione/First Lecture

Martedì 15 febbraio 11:00-12:45 Aula  Fib X1

ATTENZIONE! In precedenza era stato indicato erroneamente il giorno lunedi.

Gli interessati sono invitati a partecipare in presenza o in remoto in vista di possibili cambiamenti di orario.

Please attend, possible timetable changes will be discussed.

Pregherei anche di inviare appena possibile nome/cognome/email/matricola/corso di laurea o dottorato a ugo@di.unipi.it.

Please send name/surname/email/matricola/curriculum to ugo@di.unipi.it

Finalità del Corso

Verranno presentate alcune proprietà fondamentali dei modelli di calcolo, come la semantica operazionale ed astratta, la struttura dei tipi, l'ordine superiore, la concorrenza, l'interazione. Verranno utilizzate la semantica algebrica ed alcuni elementi della teoria delle categorie, ma non vi sono prerequisiti eccetto una conoscenza elementare dell'algebra e della logica.

Course Overview

Some basic properties of models of computation are studied, like operational and abstract semantics, typing, higher order, concurrency, interaction. Algebraic semantics and elementary category theory are employed, but no prerequisites are required except for some elementary knowledge of logic and algebra. 

Programma del Corso

• I fondamenti logici e algebrici della Computer Science
• Il lambda calcolo con tipi semplici
• L'isomorfismo di Curry-Howard
• Il PCF e il suo modello cpo, con applicazione ai linguaggi di programmazione funzionali
• Elementi di tipi ricorsivi e polimorfi, con applicazione ai linguaggi di programmazione orientati agli oggetti
• Le categorie come algebre parziali
• Categorie monoidali, cartesiane e cartesiane chiuse (CCC)
• Le CCC come modelli del lambda calcolo con tipi semplici
• Specifiche algebriche, categorie di modelli e aggiunzioni
• Le reti di Petri e i loro modelli monoidali (strettamente) simmetrici
• I sistemi di riscrittura etichettati (LTS) come coalgebre
• I sistemi LTS composizionali come bialgebre
• Il Calculus for Communicating Processes (CCS) e i suoi modelli bialgebrici
• Il Pi-Calcolo e i suoi modelli coalgebrici a prefasci
• History-Dependent Automata
• Programmazione Logica
• Quantum processes

Course Program

• Logic and algebraic foundations of computer science
• Simply typed lambda calculus
• Curry-Howard isomorphism
• PCF and its cpo model, with applications to functional programming languages
• Elements of recursive and polymorphic types, with applications to object oriented programming languages
• Categories as partial algebras
• Monoidal, cartesian and cartesian closed (CCC) categories
• CCC as models of simply typed lambda calculus
• Algebraic specifications, categories of models and adjunctions
• Petri nets and their (strictly) symmetric monoidal models
• Labelled Transition Systems  (LTS) as coalgebras
• The Calculus for Communicating Processes (CCS) and its bialgebraic models
• The Pi-Calculus and its presheaf coalgebraic models
• History-Dependent Automata
• Logic Programming
• Quantum processes

Libro di Testo/Textbook

John Mitchell, "Foundations for Programming Languages", MIT Press, 1996. Capitoli: 2.5,4,5,7.2,9,10,11.

Orario Recupero/Additional Lectures

TBA.

Note Manoscritte/Handwritten Course Notes

Lambda Calcolo: http://www.di.unipi.it/~ugo/1.lambda.pdf.

Tipi Ricorsivi, Adeguatezza Computazionale e Tipi Polimorfi/Recursive Types, Computational Adequacy and Polymorphic Types: http://www.di.unipi.it/~ugo/2.types.pdf.

Teoria della Concorrenza/Theory of Concurrency: http://www.di.unipi.it/~ugo/3.conc.pdf

CCS, Calculus for Communicating Systems: http://www.di.unipi.it/~ugo/4.CCS.pdf

Pi-calculus: http://www.di.unipi.it/~ugo/5.picalcolo.pdf

HD Automata:http://www.di.unipi.it/~ugo/6.hdautomata

Logic Programming: http://www.di.unipi.it/~ugo/Logic Programming

Capitolo di Libro/Textbook chapter

Roberto Bruni and Ugo Montanari, Costruzioni per la Semantica Operazionale della Concorrenza : vedi http://www.di.unipi.it/~ugo/costruzioni.pdf.

Modalità d'Esame/Exam Format

The student can choose between two kinds of assessment. 

• With an oral exam, the student should demonstrate his/her ability to discuss the main course contents using the appropriate notation and terminology.
• With a public seminar, the student should demonstrate his/her ability to approach a circumscribed research problem chosen with the help of the teacher, to study the relevant literature, and to organize an effective exposition of the results.
  

Last modified: 14–02-21

E_mail: ugo@di.unipi.it