ECTS - University of Pisa
| Modules | Area | Type | Hours | Teacher(s) | |
| SEMANTICA E TEORIA DEI TIPI | 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:
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 Pi-Calculus Nominal calculi as presheafs, pi-Calculus
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.
