Strumenti Utente

Strumenti Sito


Principles for Software Composition

PSC 2018/19 (375AA, 9 CFU)

Lecturer: Roberto Bruni
web - email - phone 050 2212785 - fax 050 2212726

Office hours: Tuesday 15:00-17:00 or by appointment


The objective of the course is to present:

  • different models of computation,
  • their programming paradigms,
  • their mathematical descriptions, both concrete and abstract,
  • some intellectual tools/techniques for reasoning on models.

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, stochastic process algebras) and for proving their fundamental properties, such as termination, normalisation, determinacy, behavioural equivalence and logical equivalence. Temporal and modal logics will also be studied for the specification and analysis of programs. 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.


There are no prerequisites, but the students are expected to have some familiarity with discrete mathematics, first-order logic, context-free grammars, and code fragments in imperative and functional style.


Main text:

Other readings:

External resources:


The evaluation will be based on written and oral exams.

The written exam is not necessary if the two (written) mid-terms exams are evaluated positively.

  • First (written) mid-term exam: Wed April 3, 14:00-16:00, room L1
  • Second (written) mid-term exam: Wed June 5, 11:00-13:00, room L1

Registration to written exams (mandatory): Exams registration system

In the written exam the student must demonstrate

  • knowledge: his/her knowledge of the course material
  • problem solving: the ability to solve some exercises, and
  • organisation: the ability to organise an effective and correctly written reply.

During the oral exam the student must demonstrate

  • knowledge: his/her knowledge of the course material, and
  • understanding: the ability to discuss the reading matter thoughtfully and with propriety of expression.

Oral Exams: schedule

Date Time Name
Day DD/MM hh:mm student


  • as the course starts:
    Each student should send an email to the professor from his/her favourite email account with subject PSC18-19 and the following data
    (by doing so, the account will be included in the class mailing-list, where important announcements can be sent):
    1. first name and last name (please clarify which is which, to avoid ambiguities)
    2. enrolment number (numero di matricola)
    3. bachelor degree (course of study and university)
    4. your favourite topics in computer science (optional)

Lectures (1st part)

N Date Time Room Lecture notes Links
1 Wed 20/02 14:00-16:00 L1 Introduction to the course
2 Thu 21/02 14:00-16:00 L1 Preliminaries:
formal semantics, normalisation, determinacy, consistency, equivalence,
signatures, unification problem,
3 Fri 22/02 14:00-16:00 C1 Preliminaries:
logical systems, derivations, logic programs, goal-oriented derivations
4 Wed 27/02 14:00-16:00 L1 Exercises:
unification, goal-oriented derivations

Induction and recursion:
well-founded relations, well-founded induction, mathematical induction
5 Thu 28/02 14:00-16:00 L1 Induction and recursion:
proof of induction principle, structural induction,
termination of arithmetic expressions, determinacy of arithmetic expressions
6 Fri 01/03 14:00-16:00 C1 Induction and recursion:
structural induction over many-sorted signatures, termination of boolean expressions,
operational semantics of commands, divergence
7 Wed 06/03 14:00-16:00 L1 Induction and recursion:
induction on derivations, rule induction, determinacy of commands,
well-founded recursion, denotational semantics of arithmetic expressions
8 Thu 07/03 14:00-16:00 L1 Exercises:
induction and recursion, consistency of arithmetic expressions

Induction and recursion:
lexicographic precedence relation, Ackermann function, fixpoint equations,
operational equivalence of commands

Partial orders and fixpoints:
partial orders, Hasse diagrams, chains
9 Fri 08/03 14:00-16:00 C1 Partial orders and fixpoints:
least element, minimal element, bottom element, upper bounds,
least upper bound, chains, limits, complete partial orders, powerset completeness,
CPO of partial functions, monotonicity, continuity, Kleene's fixpoint theorem
10 Wed 13/03 14:00-16:00 L1 Partial orders and fixpoints:
immediate consequences operator, denotational semantics of commands,
fixpoint computation, consistency of commands, semantic equivalence
11 Thu 14/03 14:00-16:00 L1 Partial orders and fixpoints:
consistency of commands, semantic equivalence, compositionality
12 Fri 15/03 14:00-16:00 C1 Exercises:
well-founded recursion, posets, denotational semantics
13 Wed 20/03 14:00-16:00 L1 Haskell:
an overview
ghci session 1
14 Thu 21/03 14:00-16:00 L1 Haskell:
recursion, exercises, folds
ghci session 2
15 Fri 22/03 14:00-16:00 C1 Haskell:
application, function composition, data types, type classes, recursive data structures,
derived instances, IO actions, errors

ghci session 3
16 Wed 27/03 14:00-16:00 L1 Exercises:

syntax, type system, type checking, type inference, principal type,
canonical forms, operational semantics
17 Thu 28/03 14:00-16:00 L1 HOFL:
lazy vs eager evaluation

Domain theory:
Integers with bottom, cartesian product, projections, switching lemma
18 Fri 29/03 14:00-16:00 C1 Domain theory:
functional domains, lifting, continuity theorems, apply, fix, let notation

Consistency of HOFL:
Counterexample to completeness
Wed 03/04 14:00-16:00 L1 First mid-term written exam
Extra-ordinary exam

Lectures (2nd part)

N Date Time Room Lecture notes Links
19 14:00-16:00 Denotational semantics of HOFL:
Type consistency, substitution lemma, compositionality and other properties
20 14:00-16:00 Consistency of HOFL:
Correctness of the operational semantics,
operational convergence, denotational convergence,
operational convergence implies denotational convergence,
denotational convergence implies operational convergence (optional),
operational and denotational equivalence, correspondence for type int,
unlifted semantics
21 14:00-16:00 Exercises:
HOFL, domains
22 14:00-16:00 Erlang:
an overview
erl session
23 14:00-16:00 CCS:
Syntax, operational semantics, abstract semantics, graph isomorphism,
trace equivalence, bisimulation game
24 14:00-16:00 CCS:
strong bisimulation, strong bisimilarity, strong bisimilarity is an equivalence
25 14:00-16:00 CCS:
strong bisimilarity as a fixpoint, finitely branching processes, guarded processes,
Knaster-Tarski's fixpoint theorem, Hennessy-Milner logic
26 14:00-16:00 CCS:
strong bisimilarity is a congruence, some equational laws for strong bisimilarity,
weak bisimilarity, weak observational congruence, Milner's tau-laws, value passing,
modelling with CCS
27 14:00-16:00 Exercises:
Erlang, CCS
28 14:00-16:00 CCS:
modelling and playing with CCS (using CAAL)
CAAL examples (copy the text and paste it in the Edit panel)
29 14:00-16:00 Temporal and modal logics:
linear temporal logic (LTL), computational tree logic (CTL* and CTL), mu-calculus
30 14:00-16:00 Temporal and modal logics:
mu-calculus examples

an overview
Google Go
31 14:00-16:00 GoogleGo:
an overview

syntax and operational semantics, examples
32 14:00-16:00 Pi-calculus:
abstract semantics, early and late bisimilarities, weak bisimilarities

logics, GoogleGo
33 14:00-16:00 Exercises:

Measure theory and Markov chains:
probability space, random variables, stochastic processes,
homogeneous Markov chains, DTMC, DTMC as matrices, DTMC as PTS,
next state probability, finite path probability
34 14:00-16:00 Measure theory and Markov chains:
ergodic DTMC and steady state distribution, exponential distribution, CTMC,
infinitesimal generator matrix, embedded DTMC,
bisimilarity revisited, reachability predicate, CTMC bisimilarity, DTMC bisimilarity
35 14:00-16:00 Markov chains with actions:
reactive systems, bisimilarity for reactive systems, Larsen-Skou logic

PEPA syntax, apparent rate, PEPA operational semantics,
performance analysis
36 14:00-16:00 Exercises:
probabilistic systems
Wed 05/06 11:00-13:00 L1 Second mid-term written exam
14:00-16:00 Exam
14:00-16:00 Exam
14:00-16:00 Exam
14:00-16:00 Exam
14:00-16:00 Exam
14:00-16:00 Exam

Past courses

magistraleinformatica/psc/start.txt · Ultima modifica: 22/03/2019 alle 15:49 (3 giorni fa) da Roberto Bruni