Write a Blog >>
Thu 21 Jan 2016 16:55 - 17:20 at Grand Bay South - Track 2: Sessions and processes Chair(s): Matteo Maffei

Session types provide a means to prescribe the communication behavior between concurrent message-passing processes. However, in a distributed setting, some processes may be written in languages that do not support static typing of sessions or may be compromised by a malicious intruder, violating invariants of the session types. In such a setting, dynamically monitoring communication between processes becomes a necessity for identifying undesirable actions. In this paper, we show how to dynamically monitor communication to enforce adherence to session types in a higher-order setting that allows linear channels. We present a system of blame assignment in the case when the monitor detects an undesirable action and an alarm is raised. We prove that dynamic monitoring does not change system behavior for well-typed processes, and that one of an indicated set of possible culprits must have been compromised in case of an alarm.

Poster (poster.pdf)666KiB

Thu 21 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

16:30 - 17:45: Track 2: Sessions and processesResearch Papers at Grand Bay South
Chair(s): Matteo MaffeiSaarland University
16:30 - 16:55
Talk
Effects as sessions, sessions as effects
Research Papers
Dominic OrchardImperial College London, Nobuko YoshidaImperial College London, UK
Pre-print Media Attached
16:55 - 17:20
Talk
Monitors and Blame Assignment for Higher-Order Session Types
Research Papers
Limin JiaCarnegie Mellon University, Hannah GommerstadtCarnegie Mellon University, Frank PfenningCarnegie Mellon University
Media Attached File Attached
17:20 - 17:45
Talk
Environmental Bisimulations for Probabilistic Higher-Order Languages
Research Papers
Davide SangiorgiUniversity of Bologna, Valeria VignudelliUniversity of Bologna/INRIA
Media Attached