Workshop on Behavioural APIsBEHAPI 2019

We present an axiomatic theory of contexts, i.e., terms with “holes”. The set of properties of such theory fits very well with weak-HOAS encoding techniques, where binders are represented by functional constants and the treatment of bound variables (alpha-conversion and renamings) is automatically dealt with by the metalanguage. Applying this solution to the encoding of a process algebra like, e.g., the pi-calculus in Coq gives rise to a full-fledged proof editor/proof assistant. Users no longer have to worry about explicitly renaming variables to avoid name clashes. Moreover, the formal representation of processes is very close to the original object language.

These features have immediate benefits during the formalization of processes bisimilarities. For instance, we succeeded in mechanizing a substantial chapter of the theory of strong late bisimilarity, which amounts essentially to Section 2 of A calculus of mobile processes by Milner, Parrow, and Walker.

All the axioms of our theory of contexts are satisfied in a categorical model based on presheaves, and they are compatible with the (co)inductive type theory underlying the Coq system.

Ivan Scagnetto

University of Udine

Most programming languages providing support for modifying an application’s behavior at run time run on top of a Virtual Machine (VM). In general, the VM is inaccessible for the applications. We argue that the lack of means for applications to interact with the VM limits the adaptation capabilities of running programs. To overcome this situation we explore an API (in the form of a metaobject protocol) which provides support for applications to observe and modify their underlying VM to changing requirements. We implement this API and assess how it deals with unanticipated dynamic adaptation scenarios for security, optimization, and profiling aspects. In contrast to existing alternatives, our approach is able to handle all adaptation scenarios, using less code, and without interfering with the application’s logic.

Guido Chari

Czech Technical University, Czechia

Czech Republic

Formal proofs of the meta-theory of programming calculi are important tools to develop a trust-worthy theoretical base. The meta-theory of systems with session types is delicate and error prone. I will talk about an approach to mechanise such proofs in the Coq proof assistant. In particular, I want to discuss some subtle aspects around the adequacy around a particular choice of representation, in particular some lessons learned in the process. And finally, offer a glimpse on the things we want to try in the future. This is joint work with Nobuko Yoshida.

Francisco Ferreira

Imperial College London

We overview the obligations that each site leader and participant needs to observe. We also go over the services offered by the BehAPI website and explain how to use them.

Caroline Caruana

University of Malta

We review the consotrium performance for Year 1 and coordinate the work that needs to be carried out in Year 2.

Adrian Francalanza

University of Malta

Malta

Ornela Dardha

University of Glasgow

United Kingdom

I am a Lecturer (Assistant Professor) at the School of Computing Science, University of Glasgow, UK.

I obtained my PhD in Computer Science in May 2014 from University of Bologna, Italy, under the supervision of Davide Sangiorgi. My PhD thesis Type Systems for Distributed Programs: Components and Sessions won the prize for the Best Italian PhD Thesis in Theoretical Computer Science 2015, awarded by the Italian Chapter of EATCS.

I obtained my BSc in 2008 and my MSc in 2010 in Computer Science, both summa cum laude, from Sapienza University of Rome, Italy.

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.

Wen Kokke

University of Edinburgh

United Kingdom

We propose a type system for reasoning on protocol conformance and deadlock freedom in networks of processes that communicate through unordered mailboxes. We model these networks in the mailbox calculus, a mild extension of the asynchronous pi-calculus with first-class mailboxes and selective input. The calculus subsumes the actor model and allows us to analyze networks with dynamic topologies and varying number of processes possibly mixing different concurrency abstractions. Well-typed processes are deadlock free and never fail because of unexpected messages. For a non-trivial class of them, junk freedom is also guaranteed. We illustrate the expressiveness of the calculus and of the type system by encoding instances of non-uniform, concurrent objects, binary sessions extended with joins and forks, and some known actor benchmarks.

Ugo de'Liguoro

Università di Torino

Luca Padovani

University of Turin

Italy

In this talk, I will tell about my short experience on learning the basics of proof-mechanisation in the Coq poof assistant. As an example, I will show how I mechanised cut admissibility for the multiplicative fragment of intuitionistic linear logic.

Marco Carbone

IT University of Copenhagen