ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic

In this talk, I’ll my work on a formalisation of the session-typed functional language GV using Agda. There are two main challenges which set formalising session-typed languages apart from, e.g., formalising the standard lambda calculus: First, session-typed are linear. Enforcing linearity in a formalisation is a difficult task. Worse, most available frameworks for binding (ACMM, autosubst, Ott, to name a few) do not support linear types, leaving us to solve a more difficult problem with fewer tools. My approach formalising GV is based on a combination of ACMM with Quantitative Type Theory. Second, the proof of progress for session-typed languages is complex, as configurations of processes are identified up to a structural congruence (for instance, (P | Q) = (Q | P)). While the reduction relation itself is easy to formalise, proving progress requires us to prove that we always have a pair of processes ready to communicate somewhere within the configuration. I am tackling this problem by taking some inspiration from abstract machines, and developing a syntax for configurations which is is always in normal form and which enforces the invariants which I need to prove progress.

Sat 6 Apr
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:30
Mechanising Proofs for Behavioural Types and ProcessesBEHAPI at S4 (BEHAPI)
Chair(s): Antonio RavaraNOVA University of Lisbon and NOVA LINCS
09:00
30m
Talk
A Theory of Contexts for Higher-Order Encodings of Process Algebras
BEHAPI
Ivan ScagnettoUniversity of Udine
09:30
30m
Talk
Formalising session-typed languages without worries
BEHAPI
Wen KokkeUniversity of Edinburgh
10:00
30m
Talk
Adventures in Formalising the Meta-Theory of Session Types
BEHAPI
Francisco FerreiraImperial College London