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


  • 08/05/2019:
    The missed lecture of friday 03/05 has been rescheduled as follows:
    • Wednesday 15/05 from 16:00 to 17:00 in room L1.
    • Wednesday 22/05 from 16:00 to 17:00 in room L1.
  • 02/05/2019:
    The lecture of friday 03/05 is canceled due to an institutional meeting, it will be rescheduled in May
  • 17/04/2019:
    The missed lecture of friday 29/03 is rescheduled for today from 16:00-18:00 in room L1.
  • 29/03/2019:
    Today lecture is canceled, it will be rescheduled in April
  • 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
17 Thu 28/03 14:00-16:00 L1 HOFL:
canonical forms, operational semantics, lazy vs eager evaluation

Domain theory:
Integers with bottom, cartesian product, projections
- Fri 29/03 14:00-16:00 C1 Canceled, to be rescheduled
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
18 Wed 10/04 14:00-16:00 L1 Domain theory:
switching lemma, functional domains, lifting, continuity theorems, apply
19 Thu 11/04 14:00-16:00 L1 Domain theory:
fix, let notation

Denotational semantics of HOFL:
Type consistency, substitution lemma, compositionality and other properties
20 Fri 12/04 14:00-16:00 C1 Consistency of HOFL:
Counterexample to completeness, 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 Wed 17/04 14:00-16:00 L1 Exercises:
HOFL, domains
22 Wed 17/04 16:00-18:00 L1 Erlang:
an overview
erl session
23 Thu 02/05 14:00-16:00 L1 CCS:
Syntax, operational semantics, abstract semantics, graph isomorphism,
trace equivalence, bisimulation game
- Fri 03/05 14:00-16:00 C1 Canceled, to be rescheduled
24 Wed 08/05 14:00-16:00 L1 CCS:
strong bisimulation, strong bisimilarity, strong bisimilarity is an equivalence,
strong bisimilarity as a fixpoint
25 Thu 09/05 14:00-16:00 L1 CCS:
finitely branching processes, guarded processes,
Knaster-Tarski's fixpoint theorem, Hennessy-Milner logic,
strong bisimilarity is a congruence
26 Fri 10/05 14:00-16:00 C1 CCS:
some equational laws for strong bisimilarity,
weak bisimilarity, weak observational congruence, Milner's tau-laws, value passing,
modelling with CCS
27 Wed 15/05 14:00-17:00 L1 Exercises:
Erlang, CCS

modelling and playing with CCS (using CAAL)
CAAL session 1 (copy the text and paste it in the Edit panel)
28 Thu 16/05 14:00-16:00 L1 CCS:
modelling and playing with CCS (using CAAL)
CAAL session 2 (copy the text and paste it in the Edit panel)

Temporal and modal logics:
linear temporal logic (LTL)
29 Fri 17/05 14:00-16:00 C1 Temporal and modal logics:
computational tree logic (CTL* and CTL), mu-calculus
30 Wed 22/05 14:00-17:00 L1 GoogleGo:
an overview

syntax and operational semantics, examples
Google Go
31 Thu 23/05 14:00-16:00 L1 Pi-calculus:
abstract semantics, early and late bisimilarities, weak bisimilarities

Measure theory and Markov chains:
probability space, random variables, stochastic processes,
homogeneous Markov chains, DTMC
32 Fri 24/05 14:00-16:00 C1 Exercises:
logics, GoogleGo, pi-calculus
33 Wed 29/05 14:00-16:00 Measure theory and Markov chains:
DTMC as matrices, DTMC as PTS, next state probability, finite path probability,
ergodic DTMC and steady state distribution, exponential distribution, CTMC,
infinitesimal generator matrix, CTMC stationary distribution, bisimilarity revisited,
reachability predicate, CTMC bisimilarity

probabilistic systems
34 Thu 30/05 14:00-16:00 Measure theory and Markov chains:
embedded DTMC, DTMC bisimilarity

Markov chains with actions:
reactive systems, bisimilarity for reactive systems, Larsen-Skou logic

PEPA syntax, apparent rate, PEPA operational semantics,
performance analysis

probabilistic systems
- Fri 31/05 14:00-16:00 Canceled, due to a strike of Polo Fibonacci personnel
Wed 05/06 11:00-13:00 L1 Second mid-term written exam
Wed 19/06 14:00-16:00 L1 Exam
Fri 05/07 14:00-16:00 L1 Exam
Tue 23/07 14:00-16:00 L1 Exam
Tue 10/09 14:00-16:00 L1 Exam
Thu 14/11 09:00-11:00 L1 Appello straordinario
Tue 14/01 14:00-16:00 N1 Exam
Tue 11/02 14:00-16:00 N1 Exam

Past courses

magistraleinformatica/psc/2018-19/start.txt · Ultima modifica: 11/02/2020 alle 07:30 (3 anni fa) da Roberto Bruni