|
|
- 11/02/04
-
- 29/01/04
- 04/02/04
-
-
- 29/01/04
-
- 27/01/04
-
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:
Languages
- Inductive syntax
- Syntactic techniques: variables, alpha-renaming
- Operational semantics: Reduction systems, labelled transition systems
- Lambda Calculus, Calculus for Communicating Systems (CCS), Pi Calculus
Programming
- Sequential (functional) programming
- Concurrency and non-determinism
- Synchronization constructs
- Scala (+ pilib)
Theory
- Program Equivalences
- Simulation and Bisimulation
- (Reachability analysis)
- Proof Techniques
- Using the ABC
References:
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)
(pc-selection-mode)
(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).
Professors:
Assistants:
|
