ECTS - University of Pisa
| Modules | Area | Type | Hours | Teacher(s) | |
| FOUNDATION OF COMPUTING | INF/01 | LEZIONI | 48 |
|
Students are expected to learn the essential properties of some widely employed models of computation for higher order, concurrency, interaction, mobility. Algebraic semantics and elementary category theory are employed.
The student can choose between two kinds of assessment.
(i) With an oral exam, the student should demonstrate his/her ability to discuss the main course contents using the appropriate notation and terminology.
(ii) 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.
Methods:
Delivery: face to face
Learning activities:
Attendance: Advised
Teaching methods:
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
Milner Calculus for Communicating Processes (CCS)
Labelled Transition Systems (LTS) as coalgebras
Compositional LTS as bialgebras, CCS
The Pi-Calculus and its presheaf coalgebraic models
HD Automata
Quantum processes
John Mitchell, "Foundations for Programming Languages", MIT Press, 1996. Chapters: 2.5,4,5,7.2,9,10,11.
Roberto Bruni, Ugo Montanari, Costruzioni per la Semantica Operazionale della Concorrenza, in: Claudio Bartocci e Piergiorgio Odifreddi, Eds., La Matematica, Vol. 4, Pensare il Mondo, Einaudi, 2010, or equivalent papers in English.
Handwritten notes by the teacher.
