Slides and Online Material

1. Introduction (Slides)

   Non-determinism and concurrency, powerdomains, the guarded command language, concurrency and resumption semantics.

2. The UNITY Model (Slides)

   A search for a foundation of parallel programming, introduction to the theory, an example: scheduling a meeting, a programming notation.

3. The UNITY Programming Logic (Slides)

   Introduction, basic concepts, a model of program execution, a complete example, theorems about the fundamental concepts, proving bounds on progress.

4. Programming in UNITY (Slides)

   Maximum of a set of numbers, Gaussian elimination, program structuring, program composition by union, superposition.

5. The Temporal Logic of Actions (TLA) I (Slides)

   Logic versus programming, the logic of actions, simple temporal logic, the raw logic, TLA.

6. The Temporal Logic of Actions (TLA) II (Slides)

   Invariance and eventuality properties, another example, hiding variables, further comments.

7. Conjunction of Concurrent System Specifications I (Slides)

   An informal overview, preliminaries.

8. Conjunction of Concurrent System Specifications II (Slides)

   Decomposing a complete specification, composing assumption/guarantuee specifications.

9. A Calculus of Communicating Systems (CCS) I (Slides)

   Motivation and examples, action and transition, composite actions, transition graphs, the basic language, transition rules, derivatives and derivation trees, the value passing calculus.

10. A Calculus of Communicating Systems (CCS) II (Slides)

    Strong bisimulation and strong equivalence, experimenting upon agents, (weak) bisimulation and observation equivalence, observation congruence.

11. The pi-Calculus

    Introduction, the monadic pi-calculus, applications.

12. The Polyadic pi-Calculus

    Abstractions, concretions, syntax, structural congurence and reduction, sorts, data structures and functions.