計算機言語システム論 (2023年度Aセメスター)

• 担当教員：小林直樹
• 講義日：火曜３限（13:00-14:45）
• 講義室：理学部7号館007講義室（初回のみオンラインで実施。URLはITC-LMCSに掲載）
• 休講:
• Contact：
• 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)

    Sample inputs for CAAL (Concurrency Workbench, Aalborg Version)

    • Two-place buffer
    • Alternating bit protocol
  • CCS: modal logics for processes

    Sample inputs for verification of Peterson's algorithm

    • CCS description of the algorithm
    • Mutual exclusion property
  • pi-calculus: syntax and operational semantics
  • pi-calculus: process equivalence
  • pi-calculus: type systems and typed process equivalence

    The tool TyPiCal, demonstrated in the lecture, is available here.

  • spi-calculus and verification of security protocols
• About homework:

  Homework assignments will be announced through ITC-LMS, and reports on them should also be submitted through ITC-LMS. Plagiarism is strictly prohibited. See also this page.