This course introduces concepts and techniques in the study of advanced programming languages, as well as their formal logical underpinnings. The central theme is the view of individual programs and whole languages as mathematical entities about which precise claims may be made and proved. The course will cover the basic techniques for assigning meaning to programs with higher-order, concurrent and probabilistic features (e.g., domain theory, logical systems, well-founded induction, structural recursion, labelled transition systems, Markov chains, probabilistic reactive systems) and for proving their fundamental properties, such as termination, normalisation, determinacy, behavioural equivalence and logical equivalence. In particular, some emphasis will be posed on modularity and compositionality, in the sense of guaranteeing some property of the whole by proving simpler properties of its parts. Emphasis will be placed on the experimentation of the introduced concepts with state-of-the-art tools.

• Introduction and background [1 CFU]
• Induction and recursion, partial orders, fixed points, lambda-notation [1 CFU]
• Functional programming with Haskell and analysis of higher-order functional languages [1 CFU theory and 1 CFU exercises and experimentation]
• Concurrent programming with Google Go and Erlang and analysis of concurrent and non-deterministic systems [2 CFU theory and 1 CFU exercises and experimentation]
• Code orchestration with Orc and analysis of coordination languages [1 CFU theory and experimentation]
• Models and analysis of probabilistic and stochastic systems [1 CFU theory and experimentation]