Indice

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


Objectives

The objective of the course is to present:

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.


Prerequisites

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.


Textbook(s)

Main text:

Other readings:

External resources:


Exams

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.

Registration to written exams (mandatory): Exams registration system

In the written exam the student must demonstrate

During the oral exam the student must demonstrate


Oral Exams: schedule

Date Time Name
Day DD/MM hh:mm student

Announcements


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
Haskell
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:
Haskell

HOFL:
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
Erlang
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

CCS:
modelling and playing with CCS (using CAAL)
CAAL session 1 (copy the text and paste it in the Edit panel)
CAAL
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
go-session

Pi-calculus:
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


Exercises:
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:
PEPA syntax, apparent rate, PEPA operational semantics,
performance analysis


Exercises:
probabilistic systems
PEPA
- 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