- 担当教員：小林直樹
- 講義日：火曜２限（10:25-12:10）
- 講義室：理学部7号館１０２号室
- 休講: 12/12
- 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, which will be announced in 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: modal logics for processes
- 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
- bisimulations for lambda-calculus; a note on Howe's method

- Homework
- Homework 1 (deadline: 10:25am, 3 Oct.): See the last but one page of the slides from the first lecture.
- Homework 2 (deadline: 10:25am, 10 Oct.): See the last page of the slides from the second lecture.
- Homework 3 (deadline: 10:25am, 17 Oct.): See the last page of the slides from the third lecture.
- Homework 4 (optional, deadline: 10:25am, 17 Dec.): See page 25 of the slides from the fourth lecture.
- Homework 5 (deadline: 10:25am, 31 Oct.): See page 11 of the slides on Hennessy-Milner logic.
- Homework 6 (deadline: 10:25am, 7 Nov.): See page 22 of the slides on modal logics.
- Homework 7 (deadline: 10:25am, 21 Nov.): See page 39 of the slides on modal logics.
- Homework 8 (deadline: 10:25am, 28 Nov.): See this slide.
- Homework 9 (deadline: 10:25am, 5 Dec.): See this slide.
- Homework 10 (deadline: 10:25am, 19 Dec.): See this slide.
- Homework 11 (deadline: 10:25am, 16 Jan.): See this slide.

- 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.

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