Invited talks

This year's invited speaker are:

Modular verification of concurrent programs using session types and separation logic
Jesper Bengtson(IT University of Copenhagen)

Abstract: Session types and separation logic are two leading methodologies for software verification. Session types allow users to write protocols that concurrent programs must adhere to; a session type specifies the order in which messages have to be exchanged, and the types of the data those messages carry. By checking that programs follow compatible session types, we can reason about the ways processes interact, ultimately guaranteeing the absence of deadlocks and race conditions in sessions. Separation logic is an extension of Hoare logic that is typically used to prove full functional correctness of sequential stateful programs; using separation logic, we can write pre- and post-conditions for program statements that use mutable stores such as a heap and modularly verify that they satisfy these specifications. Separation logic is more expressive than session types when it comes to data: with it we can state properties such as "x is a number greater than five", whereas session types can only express that "x is a number". On the other hand, session types offer a powerful means of checking that the communications among concurrent programs do not interfere with each other or deadlock. In this talk we describe a merger of session types and a higher-order separation logic by extending a Java-like programming language with send, receive, and fork primitives and adding session types to the Hoare logic. We combine the two methodologies to verify that a system of concurrent programs performs some communications to reach a common goal, which we define using separation logic assertions on their respective mutable stores. This allows us to verify programs like distributed sorting algorithms, where an agent can receive a list and later send a sorted version of that list. All other commands, such as loops, memory accesses and function calls are handled using separation logic in the usual way. We also maintain modular verification, as each agent is individually verified as if it were a sequential program.
This is a joint work with Morten Fangel Jensen and Fabrizio Montesi.

Idris: Implementing a Dependently Typed Programming Language
Edwin Brady (University of St Andrews)

Abstract: Idris is a purely functional programming language with dependent types. As well as supporting theorem proving, Idris is intended to be a general purpose programming language. As such, it provides high-level concepts such as implicit syntax, type classes and "do" notation. Many components of a dependently-typed programming language are by now well understood, for example the underlying type theory, type checking, unification and evaluation. How to combine these components into a realistic and usable high-level language is, however, folklore, discovered anew by successive language implementors. In this talk, I will give an overview of the implementation of Idris, showing how these it brings these components together into a complete programming language. I will briefly describe the high-level language and the underlying type theory, and present a tactic-based method for elaborating concrete high-level syntax with implicit arguments and type classes into a fully explicit core type theory. Furthermore, I will show how this method facilitates the implementation of new high-level language constructs.

A Framework for the Verified Transformation of Functional Programs
Gopalan Nadathur (University of Minnesota)

Abstract: The compilation of functional programs relies on transformations that simplify their structure while ostensibly preserving their meanings. We argue that the combination of the lambda Prolog language and the Abella interactive theorem-prover provide a natural framework for the verified implementation of such transformations. Underlying this argument is the fact that the transformations are syntax-directed and rule-based, with the important proviso that they pay attention to and also modify the binding structure of programs. The logic of higher-order hereditary Harrop formulas, the HoHH logic for short, is well-suited to formalizing such descriptions especially because of the support it provides for the higher-order representation of syntax. By virtue of the computational interpretation of the HoHH logic embodied in lambda Prolog, these formalizations become implementations of the corresponding transformations. The logic that underlies Abella embeds the HoHH logic and provides a complementary capability for reasoning flexibly and succinctly about the properties of specifications written in the HoHH logic. We will consider a typical functional program transformation and show how these twin capabilities can be exploited in its verified implementation; we will especially focus on demonstrating the benefits of a higher-order representation of syntax in both specification and reasoning. We will also discuss an extension to the logic underlying Abella for treating logical relations, a notion that is often needed in semantics preservation arguments.
The talk will draw on work done at various times with David Baelde, Alwen Tiu and Yuting Wang.