|
|
|
News
- 13/02/03
-
- 04/02/03
-
Overview
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.
Contents
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
- (Static semantics: Type Systems)
- Calculus for Communicating Systems (CCS)
Theory
- Program Equivalences
- Simulation and Bisimulation
- (Reachability analysis)
- Proof Techniques
Programming
- Sequential (functional) programming
- Concurrency and non-determinism
- Synchronization constructs
References:
Schedule
| Course: |
Wednesday 14:15-16:00, room INM 203 |
| Exercises: |
Wednesday 16:15-17:00, room INM 203 or IN2 |
Slides
- Week 1 (October 23).
- Introduction
- Week 2 (October 30).
- Functional Programming and Lambda Calculus
- Week 3 (November 6).
- Encoding FP in Lambda Calculus.
- Week 4 (November 13).
- CCS
- Week 5 (November 20).
- CCS - Examples
- Week 5 (addendum).
- From CCS to PiLib.
- Pilib reference:
(ps)
(ps.gz)
(2on1.ps)
(2on1.ps.gz)
(pdf)
- Week 6 (November 27).
- Pi Calculus
- Week 7 (December 4).
- Pi Calculus - Examples
- Week 8 (December 11).
- From Pi to Java and Back
- Week 10 (January 8, 2003).
- Equivalences for Concurrency
- Week 11 (January 15, 2003).
- Equivalences for CCS
- Week 12 (January 22, 2003).
- Proofs in CCS
- Week 13 (January 29, 2003).
- Equivalences for Pi Calculus
- Week 14 (February 5, 2003).
- Proofs in Pi Calculus
Exercises
Concurrency and Pilib libraries for Scala: (concurrency.scala) and (pilib.scala).
Distribution of the ABC tool.
Using Scala in the room IN2
To use Scala on the Windows machine of room IN2 you need two things:
- an text editor : for editing your files: you can use Emacs or Note Tab for instance.
- a dos prompt : in the menu, you can select "run", then enter
cmd.exe.
Now there are three different tools at your disposal:
- siris : an interactive interpreter that lets you type in your
Scala definitions (values or functions) and expressions and see
immediatly the result. To launch siris just type in
siris in
a dos window.
- surus : a non-interactive interpreter which takes as arguments a list
of Scala files (ending with the suffix
.scala) and evaluates
their contents as if they had been entered in the interactive interpreter.
To use surus just type in surus myfile.scala in a dos window.
- socos : a Scala compiler that produces java bytecodes that can then be interpreted
by a JVM.
If you use Emacs there is a Scala mode that allows you to automatically
indent and highlight your code. Just copy the file .emacs in your
home directory (i.e. the answer of the command echo %HOME% in a dos window,
by default it should be c:\temp).
Contact
Professors:
Assistants:
Related Links
|
|
-Calculus