VEST

Thursday, 4 June

Mechanized Duality for Recursive Session Types

We report on our work to mechanize proofs of equivalence for different definitions of duality proposed in the literature. This work is supporting and based on the paper "Duality of Session Types: The Final Cut" at PLACES 2020.

Mechanised Semantic Session Types

Session types are a family of type systems for message-passing concurrency, which has been subject to many extensions. Unfortunately, separate soundness proofs are developed for each extension, but these cannot be readily combined. Moreover, soundness proofs are generally not mechanized in a proof assistant, making their correctness less trustworthy. In this paper we overcome these shortcomings with a semantic approach to binary session types using a logical relations model in the Iris framework in Coq. We demonstrate the power of our approach by combining various forms of polymorphism and recursion, asynchronous subtyping, mutable and shared references, and mutexes, with little proof effort. As an additional benefit of the semantic approach we demonstrate how to integrate manual verification of racy but safe programs as part of well-typed programs.

Paper: Machine-Checked Semantic Session Typing

Gitlab Source: Actris

Towards Formalising Trace Equivalence for Global and Local Types

A formal correspondence between session types and communicating finite state automata has been studied over the last decade, playing a fundamental role to build session-based systems for, e.g., runtime monitoring and API generation. A labelled transition system (LTS) is given both for global types and local types, thus capturing their semantics. The LTS traces (sequences of performed actions) represent the evolution of a communicating system and the soundness and completeness theorems for session types are proven to show: the traces of the execution of a global type are the same as the ones obtained by the execution of the collection of its local projections. This talk will report on our formalisation experience of such theory in the Coq Proof Assistant. Starting from a straightforward inductive encoding of the syntax of global and local types, we "unroll" each type to a coinductive representation, as a possibly infinite tree. This captures the possibly infinite nature of execution, taking a first step towards semantics. We then define LTSs for global and local types on coinductive trees. Each time we take one step further into semantics---from types to trees, from trees to LTS---projections need to be preserved along the way, thus ensuring that local computation stays faithful to the global discipline.

It Takes a Village: Reasoning About Concurrent Processes

Typing disciplines offer a way to tame programs so they become more approachable and easier to reason about, both formally and by the cognitive load they require from their users. Languages like Haskell and OCaml, proof assistants like Agda and Coq are built on these premises. Session types, and particularly Multiparty Session Types (MPST), offer a typing discipline that aims at showing the safe interaction of distributed processes. In this work we want to use MPST to guide and allow us to reason about processes. Of particular importance is to reason about the trace of actions performed by processes participating in a global choreography (represented by a global type). We propose a reasoning framework in the Coq proof assistant, that necessarily builds on top of a mechanisation of the meta-theory of session types. The mechanisation of a proof is the gold standard to establish its dependability, in this work we want to show, that a mechanisation is also the foundation to build certified tools that enable us to go further.

Verifying functional correctness of message-passing programs in Coq

During this talk I will give a demo of the use of separation logic for proving functional correctness of message-passing programs in the Coq proof assistant. I will use the Actris framework (Hinrichsen et al., POPL'20), which is built on top of the Iris separation logic, and provides high-level proof principles and Coq tactics for reasoning about message-passing programs.

WorkflowFM: Correct-by-construction processes in practice

In the past few years we have developed the process modelling framework WorkflowFM. It relies on the proofs-as-processes paradigm to provide correct-by-construction workflow synthesis, with guarantees of type correctness, deadlock freedom, and rigorous resource accounting. Workflows are composed via proof and extracted as asynchronously executable terms in pi-calculus or session types. The core implementation consists of an embedding of Classical Linear Logic in HOL Light, coupled with a reasoning framework for object-level proofs and associated tactics for proof automation.

WorkflowFM has been used in practice to model and manage patient pathways in healthcare and production flows in manufacturing. This effort has introduced interesting challenges, such as persistent distributed enactment, integration with IoT data, and job-shop scheduling. This has helped form a fruitful connection between theory and practice.

Paper: WorkflowFM: A Logic-Based Framework for Formal Process Specification and Composition

GitHub Source: hol-light-embed

Approaches to Mechanising Behavioural Types

Friday, 5 June

A linear Pi calculus in Coq (wip)

Our long term objective is to develop techniques/tools and libraries to lower the cost of verifying with the Coq proof assistant results on process calculi and behavioral types. As a first step towards this objective, in collaboration with Giunti and Ravara in Lisbon and Peters in Darmstdt, we choose to mechanize proofs for a simple typed version of the pi-calculus where we want to guarantee linear usage of the communication channels. We decide to focus on the representation of binders, a well-know difficulty in mechanizing paper proofs. We have identified three different formalization techniques: De Bruijn levels, nominals and identifiers. Our objective is to finalize the description of the calculus and type system in all three techniques and to prove their equivalence.

In this talk I will present the (work in progress) formalization based on De Bruijn levels done in Coq using the SSReflect proof language.

Pi without alpha

In mobile calculi like the pi-calculus, scoped names are treated as bound and thus not externally referable. Static analyses to detect properties on them, such as those describing locks, are then not able of clearly identifying problematic channels via their names.

To overcome the situation, we developed a reformulation of the linear pi-calculus that does not assume alpha-conversion but automatically book-keeps information regarding name scoping. The semantics is defined in terms of a labelled transition system that also tracks the evolution of linear permissions. Renaming of scoped names to avoid clashes is performed with a total function generating natural numbers not used elsewhere.

Since our long term goal is the certification of the implementations of analyses algorithms to check properties on processes (i.e., to have mechanised proofs of soundness of the algorithms), we are guided by a main concern: not to introduce non-determinism unnecessarily. It usually appears in linear mobile calculi both in the semantics (mainly when structural congruence is used), and in the type systems in the type environment split relation. Our labelled transition system not only does not use alpha-conversion, but also avoids using a structural congruence relation. Keeping with existing typing tradition, the type system only uses type-splitting in the parallel composition rule, thus localising non-determinism, showed already in other work to be determinisable.

We show that in our calculus subject reduction and type-safety (a form of race-freedom) hold. The subject reduction proof is mechanised; the type safety one is underway.

Hosting a Dependently Typed Linear Pi Calculus in Agda

In this talk we report on our experience in formalizing a variant of the linear pi calculus in Agda. We represent pi calculus processes as a DSL that can access all the features of the underlying Agda layer, particularly dependent pairs and dependent pattern matching. This way, we obtain a minimal, unifying process model capable of encoding a broad family of complex session type theories, including dependent and refinement session types.

Gitlab Source: DependentLinearPi

Towards a Universe of Linear Syntaxes with Binding

Recent work by Allais et al has produced a general framework for specifying simply typed programming languages and proving metatheoretic properties about them in Agda. In particular, this framework eliminates the need to do induction over syntax in many cases, which is a big win for languages with many syntactic constructs. All of the syntaxes describable in the framework support renaming and substitution, so these lemmas need not be proven by the user.

However, the framework makes two assumptions that are apparently broken by linear type systems, as used in languages for session types. One is that contexts only grow in a typing derivation, and the other is that typing is preserved under such context growths (i.e, weakening is admissible). In this talk, I will discuss how we are refining these assumptions so as to allow for a general form of usage tracking which subsumes intuitionistic linear typing (including !). We hope that the resulting framework will be useful for prototyping session type systems, allowing such systems to be changed quickly without the need to redo boring syntactic proofs.

Paper: A Linear Algebra Approach to Linear Metatheory

GitHub Source: generic-lr

pi with leftovers: a mechanisation in Agda

The pi-calculus is a computational model for communication and concurrency. The linear pi-calculus is a typed version of the pi-calculus where channels must be used exactly once. It is an underlying theoretical and practical framework on top of which more advanced types and theories can be built, including session types.

We present the first full mechanisation in Agda of a pi-calculus with linear, graded and shared types, all under the same unified framework. While linearity is key for type safety in communication- centric programming, graded and shared types are needed to model real-world software systems. We present the syntax, semantics, type system and corresponding type safety properties. For the first time in the pi-calculus, we use leftover typing to encode our typing rules in a way that propagates linearity constraints into process continuations. We generalise the algebras on multiplicities, allowing the user to choose a mix of linear, graded and shared typing. We provide framing, weakening and strengthening theorems, which can now be stated for the linear pi-calculus and use them to prove subject congruence. We show that the type system is stable under substitution and prove subject reduction. Our formalisation is fully mechanised in Agda.

Paper: pi with leftovers: a mechanisation in Agda

GitHub Source: typing-linear-pi

Psi-calculi in Isabelle

Psi-calculi are extensions of the pi-calculus, accommodating arbitrary nominal datatypes to represent not only data but also communication channels, assertions and conditions, giving it an expressive power beyond the applied pi-calculus and the concurrent constraint pi-calculus.

We have formalised psi-calculi in the interactive theorem prover Isabelle using its nominal datatype package. One distinctive feature is that the framework needs to treat binding sequences, as opposed to single binders, in an efficient way. While different methods for formalising single binder calculi have been proposed over the last decades, representations for such binding sequences are not very well explored.

The main effort in the formalisation is to keep the machine checked proofs as close to their pen-and-paper counterparts as possible. We discuss two approaches to reasoning about binding sequences along with their strengths and weaknesses. We also cover custom induction rules to remove the bulk of manual alpha-conversions. This is joint work with Joachim Parrow.

Automatising Proofs for Multiparty Session Types

The formalisation of multiparty session types includes the proofs of their standard properties such as subject reduction. There is a huge number of different variants of multiparty session types but their subject reduction proofs are all very similar and follow the basic structure of preservation proofs of all type systems. Accordingly, it should be possible or even easy to automatise this proof. The standard proof strategy requires some auxiliary results such as the inversion of typing rules and substitution lemmata. Moreover, the proof requires to construct partial proof trees from the typing rules. In the talk I would like to analyse the strategy of a typical subject reduction proof and break it into the parts that need to be automatised in order to derive an automatic proof strategy.