Lecturer	Nobuko Yoshida
Degrees	Schedule C1 (CS&P) — Computer Science and Philosophy Schedule C1 — Computer Science Schedule C1 — Mathematics and Computer Science Michaelmas Term — MSc in Advanced Computer Science MSc in Mathematics and Foundations of Computer Science
Term	Michaelmas Term 2024  (20 lectures)

Overview

This course studies the foundations and type theory of mobile processes and programming languages for communication and distribution. Specifically, this course studies how to program communication through an introduction of a channel-based message-passing process calculus (the pi-calculus) and how to apply its type theory to practice. A course also functions as a brief introduction of message-passing programming languages such as Go language (a popular recent programming language designed by Google, which is widely used for implementing large distributed system). The course assumes a basic knowledge of programming languages. Some knowledge of concurrent programming, lambda-calculus or operational semantics would be useful but not required.

Learning outcomes

This course gives an overview of expressiveness and type theory of concurrent and distributed computations with applications to modern message passing programming languages.

• understand the syntax and operational semantics of mobile processes
• understand how to encode various higher-order concurrent data structures in mobile processes
• learn the contextual congruence of mobile processes
• learn how to program various concurrent agents and data structures in Go programming language
• learn a basic linear type theory for communications, and how to guarantee communication safety and deadlock freedom through type checking.
• learn applications of behavioural type systems for communications

Prerequisites

• Prerequisite: Concurrent Programming or some equivalent course (in any programming language)
• Desired: Operational semantics of any formalism such as lambda calculus or programming languages
• Desired: Lambda Calculus
• Desired: Concurrent Processes
• The course is recommended after or in parallel with Lambda Calculus and Types and/or Concurrency.

Synopsis

Course overview, introduction and applications of behavioural type systems of communication and distribution
• Part 1: Mobile Processes
– Syntax and operational semantics 
– Expressiveness: mobile processes and concurrent higher-order data structures 
– Go programming language and mobile processes 
– Class Room Exercises 
• Part 2: Contextual Congruence, axiomatisations and their applications 
• Part 3: Behavioural types (basic session types)
– Introduction and a usecase 
– Session types, duality and subtyping 
– Session typing system 
– Communication safety theorem and its proof 
– Class Room Exercises 
• Part 3: Advanced type theory and its applications
– Introduction of multiparty session types 
– Specification and typing system 
– Communication safety and deadlock-freedom theorems and their proofs 
– Class Room Exercises
– Scala Laboratory Exercise

Taking our courses

This form is not to be used by students studying for a degree in the Department of Computer Science, or for Visiting Students who are registered for Computer Science courses

Other matriculated University of Oxford students who are interested in taking this, or other, courses in the Department of Computer Science, must complete this online form by 17.00 on Friday of 0th week of term in which the course is taught. Late requests, and requests sent by email, will not be considered. All requests must be approved by the relevant Computer Science departmental committee and can only be submitted using this form.