Department of Information Technology
Department of Information Technology
Uppsala UniversityInformation TechnologyResearchResearch groupsConcurrency theory
Listen

Advanced process calculi, Copenhagen, August 2013

Introduction

This course focuses on advanced modelling techniques of distributed systems using Psi-calculi. Psi-calculi extend the pi-calculus with nominal datatypes for data structures and for logical assertions and conditions. These can be transmitted between processes and their names can be statically scoped as in the standard pi-calculus. Psi-calculi can capture the same phenomena as other proposed extensions of the pi-calculus such as the applied pi-calculus, the spi-calculus, the fusion calculus, the concurrent constraint pi-calculus, and calculi with polyadic communication channels or pattern matching. Psi-calculi can be even more general, for example by allowing structured channels, higher-order formalisms such as the lambda calculus for data structures, and predicate logic for assertions.

You will receive 4 ETCS for the course. You are expected to prepare by reading up on a few select papers that are given below, attend four lectures in week 34 (19th to the 23d of August), and do a small project in September using one or several of the methods taught in the course. Preferably, the project should somehow be connected to your research but this is not a strict requirement.

Prerequisites

Students are expected to have a solid understanding in logics and semantics. Proficiency in process calculi is a plus, but not a strict requirement.

Updates

  • 8/19 The room has changed to 4A22.

Schedule

The course consists of four days of lectures and labs. It begins on the 34th week, 20th of August.

Date Day Room What Who Prep. Reading Slides
8/20 10-12 1 4A22 Introduction to the pi-calculus JP An Introduction to the pi-Calculus Sec. 1, 2, 3.1-3.4, 4, 5.3, 6 and 7.1 Lecture 1
8/20 13-16 1 4A22 The pi-calculus (pen and paper) lab JP, RG pi-calculus questions
8/21 10-12 2 4A22 Introduction to the psi-calculus JP Psi-calculi: A framework for mobile processes with nominal data and logic, Ch. 1-3 Lecture 2
8/21 13-16 2 4A22 Pen and paper lab on the psi-calculus JP, RG Introductory exercises on psi-calculi
8/22 10-12 3 4A22 Bisimulation in the Psi-calculus. Introduction to the Psi-Calculi Workbench JP, RG Psi-calculi: A framework for mobile processes with nominal data and logic, Ch.5, A parametric tool for applied process calculi Lecture 3, Introduction to Pwb
8/22 13-16 3 4A22 Psi-Calculi Workbench lab RG Psi-Calculi Workbench, An Introduction to the pi-Calculus Sec. 5.2, Pwb Exercises
8/23 10-12 4 4A22 Higher Order Psi-calculi and Isabelle formalization of Psi-calculi JP, JB Sorted psi-calculi Ch 1-2, Higher-order psi-calculi, Formalising the pi-calculus using nominal logic, Sec. 1-4 Lecture 4
8/23 13-16 4 4A22 Project lab RG Psi-Calculi Workbench Appendix A

Project

The project is to formalize in Psi-calculi and implement a concurrent system of your choice in Psi-Calculi Workbench and check some property of that system with the symbolic bisimulation checker.

The project should be done during September, and submitted together with a short report (upto 4 pages) describing it.

The amount of working hours allocated for the project is 25-30 (3-4 days).

In case you want to do a different project, you can discuss that possibility with the teachers.

For those who do not speak Standard ML, these slides provide a quick introduction.

Material

Additional Material

Updated  2016-08-17 15:26:29 by Björn Victor.