Ecole Polytechnique Fédérale de Lausanne
Concurrency: Languages, Programming and Theory 2003/2004

The course aims to teach the foundations needed for the understanding of concurrent programs and reactive systems. We will cover basic techniques to describe the form and meaning of program terms and to reason about them. These techniques are applied in the discussion of CCS, a well-known calculus for reactive systems. Based on this calculus, we will discuss notions of equivalence of concurrent programs, as well as proof techniques to show equivalence or refinement. The course will be accompanied by practical programming exercises.

Three concurrent and interacting streams in the course deal with issues of languages, theory, and programming. Concepts discussed in the course include:


  • Inductive syntax
  • Syntactic techniques: variables, alpha-renaming
  • Operational semantics: Reduction systems, labelled transition systems
  • Lambda Calculus, Calculus for Communicating Systems (CCS), Pi Calculus
  • Sequential (functional) programming
  • Concurrency and non-determinism
  • Synchronization constructs
  • Scala (+ pilib)
  • Program Equivalences
  • Simulation and Bisimulation
  • (Reachability analysis)
  • Proof Techniques
  • Using the ABC


Course: Wednesday 14:15-16:00, room INR 219
Exercises: Wednesday 16:15-17:00, room INR 219 or IN1


Week 1 (October 22):
Week 2 (October 29):
Week 3 (November 5):
Week 4 (November 12):
Week 5 (November 19):
Week 6 (November 26):
Week 7 (December 3):
Week 8 (December 10):
Week 10 (January 7):
Week 11 (January 14):
  • Discussion of the Test Exam
  • Homework correction
  • Finishing off with leftovers from Week 10
  • Starting with Equivalences in CCS (pdf, ps, 4on1.ps, 8on1.ps)
Week 12 (January 21):
  • Finishing off with leftovers from Week 11
  • Proofs in CCS (pdf, ps, 4on1.ps, 8on1.ps)
  • Practicals with ABC
Week 13 (January 28):
  • Equivalences in Pi Calculus (pdf, ps, 4on1.ps, 8on1.ps)
  • if time permits, more practicals with the ABC ...
Week 14 (February 4):
Bonus Exam
This year bonus exam (correction)

Week 2 (October 29): Sieve of Erathostenes
Solution in (pdf) or (ps).
Week 3 (November 5th): Call-by-Value and Call-by-Need
Assignment in (pdf) or (ps).
Skeleton: lambdaCalculus-partial.scala.
Solution: lambdaCalculus.scala.
Week 5 (November 19): Two-place Buffer and Scheduler using Pilib
Assignment in (pdf) or (ps).
To be downloaded: pilib.scala, twoPlaceBuffer-partial.scala, scheduler-partial.scala.
Solution: twoPlaceBuffer.scala, scheduler.scala.
Week 7 (December 3): Elastic Buffer
Assignment in (pdf) or (ps).
To be downloaded: pilib.scala, elasticBuffer-partial.scala.
Solution: elasticBuffer.scala.
Week 8 (December 10): Proof by Induction
Assignment in (pdf) or (ps).
Solution in (pdf) or (ps).
Week 12 (January 21): Practising ABC
Assignment in (pdf) or (ps).
Modeling a problem in Pi (pdf) or (ps).
Files: scheduler2.abc enigme_pi.abc.
Solution: scheduler2-completed.abc enigme_pi-completed.abc
Week 14 Semaphores
Assignment in (pdf) or (ps).
Files: semaphore.scala semaphore.abc.

Help for Scala
  • To use Scala on computers in room IN1 you must modify the PATH environment variable:

    setenv PATH ${PATH}:/home/iclamp/soft/bin
  • Other instructions on how to write, compile and run your first Scala program can be found here.
  • To use the Scala emacs mode put the following lines into your .emacs file (at the root of your directory):
    (global-font-lock-mode t)
    (show-paren-mode 1)
    (blink-cursor-mode -1)
    (column-number-mode 1)
    (global-set-key [(meta control g)] 'goto-line)
    (add-to-list 'load-path (expand-file-name "~iclamp/soft/share/emacs/site-lisp"))
    (load "scala-mode-auto")

The newsgroup of the course is located at epfl.ic.cours.clpt (interface web).