- 担当教員：小林直樹
- 講義日：火曜２限（10:25-12:10）
- 講義室：理学部7号館１０２号室
- 休講: 11/10,12/1, 1/18
- Contact：
- Subjects： This year, we plan to cover process calculi (such as CCS and pi-calculus) and their applications to verification of concurrent systems/programs and security protocols.
- References:
- R. Milner, Communication and Concurrency, Prentice Hall, 1989
- R. Milner, Communicating and Mobile Systems: the p-calculus, Cambridge University Press, 1999
- D. Sangiorgi and D. Walker, The p-calculus: A Theory of Mobile Processes, Cambridge University Press, 2001
- C. Stirling, Modal and Temporal Properties of Processes, Springer, 2001

- slides and lecture notes (protected by a password, except for the slides from the first lecture)
- CCS: syntax and operational semantics
- CCS: process equivalence 1 (trace equivalence and strong bisimilulation)
- CCS: process equivalence 2 (weak bisimulation and simulation; co-induction)
- CCS: process equivalence 3 (tools and techniques for proving bisimulation; testing equivalence)
- CCS: barbed congruence, modal logics for processes
- model checking, pi-calculus: syntax and operational semantics
- pi-calculus: process equivalence
- pi-calculus: type systems and typed process equivalence
- spi-calculus and verification of security protocols
- spi-calculus 2: type-based verification of security protocols
- bisimulations for lambda-calculus; a note on Howe's method

- Homework
- Homework 1 (deadline: 10:25am, 13 Oct.): See the last page of the slides from the first lecture.
- Homework 2 (deadline: 10:25am, 20 Oct.): See the last page of the slides from the second lecture.
- Homework 3 (deadline: 10:25am, 27 Oct.): See the last page of the slides from the third lecture.
- Homework 4 (deadline: 10:25am, 17 Nov.): See page 25 of the slides from the fourth lecture.
- Homework 5 (deadline: 10:25am, 17 Nov.): See the last page of the slides from the fifth lecture.
- Homework 6 (deadline: 10:25am, 24 Nov.): See page 24 of the slides from the sixth lecture.
- Homework 7 (deadline: 10:25am, 8 Dec.): See page 25 of the slides from the seventh lecture.
- Homework 8 (deadline: 10:25am, 15 Dec.): See page 29 of the slides from the eighth lecture.
- Homework 9 (deadline: 10:25am, 22 Dec.): See last page of the slides from the ninth lecture.
- Homework 10 (deadline: 10:25am, 12 Jan.): See page 12 of the slides from the eleventh lecture.

- About homework:
Reports can be submitted either by email (see the contact mail addres above), or by hand (at the time of the lecture). The deadline is the beginning of the next lecture, unless specified otherwise. The deadline is strict.

If you submit a report via email, please send it as a plain text or PDF file as long as possible. If you send multiple files, attach them either as separate files (if the number of files is no more than 3) or as a zip archive. The size of files should not exceed 2 Mbyte; if it does, please consult me on a procedure to submit the report.

**他人のものを写したものを提出する等の不正が見つかった場合には，試験の際のカンニングに準じて，厳罰を適用します． こちらのページのレポートに関する注意も確認すること．**