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: TBA
  • Second (written) mid-term exam: TBA

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, logical systems, derivations
3 Fri 22/02 14:00-16:00 C1 Preliminaries:
signatures, unification problem, logic programs
goal-oriented derivations
4 14:00-16:00 Exercises:
unification, goal-oriented derivations

Induction and recursion:
well-founded relations, well-founded induction, mathematical induction
5 14:00-16:00 Induction and recursion:
proof of induction principle, structural induction,
termination of arithmetic expressions, determinacy of arithmetic expressions
6 14:00-16:00 Induction and recursion:
structural induction over many-sorted signatures, termination of boolean expressions,
operational semantics of commands, divergence
7 14:00-16:00 Induction and recursion:
induction on derivations, rule induction, determinacy of commands,
well-founded recursion, lexicographic precedence relation, Ackermann function,
denotational semantics of arithmetic expressions, fixpoint equations
8 14:00-16:00 Exercises:
induction and recursion, consistency of arithmetic expressions

Partial orders and fixpoints:
partial orders, Hasse diagrams, least upper bound, chains, limits,
complete partial orders, bottom element, powerset completeness
9 14:00-16:00 Partial orders and fixpoints:
CPO of partial functions, monotonicity, continuity, Kleene's fixpoint theorem
10 14:00-16:00 Exercises:
induction, recursion, posets

Partial orders and fixpoints:
immediate consequences operator, denotational semantics of commands
11 14:00-16:00 Partial orders and fixpoints:
fixpoint computation, consistency of commands, semantic equivalence
12 14:00-16:00 Haskell:
an overview
ghci session 1
13 14:00-16:00 Haskell:
recursion, folds, application, function composition
ghci session 2
14 14:00-16:00 Haskell:
data types, type classes, recursive data structures, derived instances,
IO actions, errors

ghci session 3
15 14:00-16:00 Exercises:
well-founded recursion, posets, denotational semantics, Haskell
16 14:00-16:00 HOFL:
syntax, type system, type checking, type inference, principal type,
canonical forms, operational semantics
17 14:00-16:00 First mid-term written exam
Extra-ordinary exam

Lectures (2nd part)

N Date Time Room Lecture notes Links
18 14:00-16:00 HOFL:
lazy vs eager evaluation

Domain theory:
Integers with bottom, cartesian product, projections, switching lemma
19 14:00-16:00 Domain theory:
functional domains, lifting, continuity theorems, apply, fix, let notation

Consistency of HOFL:
Counterexample to completeness
20 14:00-16:00 Denotational semantics of HOFL:
Type consistency, substitution lemma, compositionality and other properties
21 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
22 14:00-16:00 Exercises:
HOFL, domains
23 14:00-16:00 Erlang:
an overview
erl session
24 14:00-16:00 CCS:
Syntax, operational semantics, abstract semantics, graph isomorphism,
trace equivalence, bisimulation game
25 14:00-16:00 CCS:
strong bisimulation, strong bisimilarity, strong bisimilarity is an equivalence
26 14:00-16:00 CCS:
strong bisimilarity as a fixpoint, finitely branching processes, guarded processes,
Knaster-Tarski's fixpoint theorem, Hennessy-Milner logic
27 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
28 14:00-16:00 Exercises:
Erlang, CCS
29 14:00-16:00 CCS:
modelling and playing with CCS (using CAAL)
CAAL examples (copy the text and paste it in the Edit panel)
30 14:00-16:00 Temporal and modal logics:
linear temporal logic (LTL), computational tree logic (CTL* and CTL), mu-calculus
31 14:00-16:00 Temporal and modal logics:
mu-calculus examples

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

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

logics, GoogleGo
34 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
35 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
36 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
37 14:00-16:00 Exercises:
probabilistic systems
38 14:00-16:00 Second mid-term written exam
39 14:00-16:00 Exam
40 14:00-16:00 Exam
41 14:00-16:00 Exam
42 14:00-16:00 Exam
43 14:00-16:00 Exam
44 14:00-16:00 Exam

Past courses

magistraleinformatica/psc/start.txt · Ultima modifica: 13/02/2019 alle 15:25 (7 giorni fa) da Roberto Bruni