Welcome to the 6th South of England Regional Programming Language Seminar.
S-REPLS is a regular and informal meeting for those based in the South of England with a professional interest—whether it be academic or commercial—in the semantics and implementation of programming languages.
The seminar is free of charge and lunch will be provided.
Date and Location
The 6th edition of S-REPLS will take place on May 25, 2017, at University College London.
The seminar will take place at the Room 421 of Roberts
Building, 1-19, Torrington Pl.
You can find here the directions to the campus.
UCL Roberts Building
To register to attend S-REPLS 6, please fill out your name and check the “Seminar” column on the following Doodle poll:
If you plan to attend the pay-your-own-way dinner after the seminar, please check the “Dinner” column. If you have any dietary restrictions, please email us.
- 9:30-10:00 - Welcome refreshments
- 10:00-11:00 - Keynote
- 11:00-12:00 - Regular Talks
◦ 11:00-11:30: A framework for verifying Conflict-free Replicated Data Types (CRDTs)
Dominic Mulligan, University of Cambridge
We present a framework for verifying the convergence of Conflict-free Replicated Data Types (CRDTs). Working above an axiomatic model of causal asynchronous networks, we prove an abstract convergence theorem which we claim is the "essence" of why operation-based CRDTs converge. As corollaries of this abstract convergence theorem, we obtain concrete convergence theorems for specific implementations of CRDTs, such as the Replicable Growable Array (RGA). All proofs are checked in Isabelle/HOL.
This is joint work with Martin Kleppmann, Victor Gomes, and Alastair Beresford.
◦ 11:30-12:00: Lightweight Session Programming in Scala
Alceste Scalas, Imperial College London
Designing, developing and maintaining concurrent applications is an error-prone and time-consuming task; most difficulties arise because compilers are usually unable to check whether the inputs/outputs performed by a program at runtime will adhere to a given protocol specification. To address this problem, we leverage the native features of the Scala programming language, type system and standard library, to introduce (1) a representation of protocols (session types) as Scala types, and (2) a library, called lchannels, with a convenient API for type-safe protocol-based programming, supporting local and distributed communication.
- 12:00-13:30 - Lunch
- 13:30-15:30 - Regular Talks
◦ 13:30-14:00: Whiley: a Platform for Research in Verifying Compilers
David J. Pearce, Victoria University of Wellington
The Whiley programming language and verifying compiler have been under development since 2009. The language itself was designed with verification in mind, and certain choices reflect this. For example, the use of unbound arithmetic and structural typing. The language also has some other notable features, such as the use of flow typing with union, intersection and negation types. Furthermore, Whiley has recently gained support for reference lifetimes, similar to those found in Rust. Reference lifetimes open up more possibilities in terms of both verification and efficient implementation.
In this talk, I'll demonstrate the system being used to verify some useful programs. I'll also examine and reflect on some of the interesting technical challenges faced so far. For example, the implementation of recursive structural types with unions, intersections and negations turned out to surprisingly involved. Likewise, the system includes a purpose-built automated theorem prover which has proved (unsurprisingly) to be an interesting challenge.
◦ 14:00-14:30: Automatic Enforcement of Expressive Security Policies using Enclaves
Anitha Gollamudi, Harvard University
Hardware-based enclave protection mechanisms, such as Intel’s SGX, ARM’s TrustZone, and Apple’s Secure Enclave, can protect code and data from powerful low-level attackers. In this work, we use enclaves to enforce strong application-specific information security policies.
We present IMPE, a novel calculus that captures the essence of SGX-like enclave mechanisms, and show that a security-type system for IMPE can enforce expressive confidentiality policies (including erasure policies and delimited release policies) against powerful low-level attackers, including attackers that can arbitrarily corrupt non-enclave code, and, under some circumstances, corrupt enclave code.
We present a translation from an expressive security-typed calculus (that is not aware of enclaves) to IMPE. The translation automatically places code and data into enclaves to enforce the security policies of the source program.
◦ 14:30-15:00: An axiomatic framework for weakly-consistent transactional memory
Nathan Chong, ARM Cambridge
Modern multiprocessors typically provide memory models that are weaker than sequential consistency, and much work has been done by the programming languages community to formalise and prove theorems about these models for a variety of architectures.
Several modern multiprocessors also provide transactional memory (TM), such as Intel's Haswell and IBM's Power8. Much work has been done to study the semantics of TM in a sequentially-consistent setting, but the precise guarantees TM provides in a weak memory setting have received little attention. In this work, we investigate how the axiomatic approach for modelling weakly-consistent memory can be extended to handle TM, with particular reference to the ARM and Power architectures.
We follow a novel iterative methodology for developing models of TM in a weak memory setting. Given the current iteration of the model and a possible refinement of it, we use a constraint-solver to generate all litmus tests (of a bounded size) that differentiate the two. We then decide whether to accept the refinement by examining these tests, discussing them with microarchitectural engineers, and running them on available hardware.
This work is a collaboration between Nathan Chong (ARM Cambridge), Tyler Sorensen (Imperial) and John Wickerson (Imperial).
◦ 15:00-15:30: Model checking based analysis of Go programs
Nicholas Ng, Imperial College London
Go is a production-level statically typed programming language whose design features explicit message-passing primitives and lightweight threads, enabling (and encouraging) programmers to develop concurrent systems where components interact through communication more so than by lock-based shared memory concurrency. Go can detect global deadlocks at runtime, but does not provide any compile-time protection against all too common communication mismatches and partial deadlocks.
In this work we present a static verification framework for liveness and safety in Go programs, able to detect communication errors and deadlocks by model checking. Our toolchain infers from a Go program a faithful representation of its communication patterns as behavioural types, where the types are model checked for liveness and safety.
This is joint work with Julien Lange, Bernardo Toninho, and Nobuko Yoshida.
- 15:30-16:15 - Coffee Break
- 16:15-17:45 - Regular Talks
◦ 16:15-16:45: A Categorical Automata Learning Framework (CALF)
Matteo Sammartino, University College London
Automata learning is a technique to learn an automaton model of a black-box system from observations. It has successfully been applied in verification, with the automaton type varying depending on the application domain. Adaptations of automata learning algorithms for increasingly complex types of automata have to be developed from scratch because there is no abstract theory offering guidelines. This makes it hard to devise such algorithms, and it obscures their correctness proofs.
In this talk I will present CALF, an abstract framework for studying automata learning algorithms in which specific instances, correctness proofs, and optimizations can be derived without much effort.
◦ 16:45-17:15: Lambda Calculus in Core Aldwych
Matthew Huntbach, Queen Mary University of London
Core Aldwych is a simple model for concurrent computation, involving the concept of agents that communicate through shared variables. Each variable will have exactly one agent that can write to it, and its value can never be changed once written, but a value can contain further variables that are written to later. A key aspect is that the reader of a value may become the writer of variables in it. In this paper we show how this model can be used to encode lambda calculus. Individual function applications can be explicitly encoded as lazy or not, as required. We then show how this encoding can be extended to cover functions that manipulate mutable variables, but with the underlying Core Aldwych implementation still using only immutable variables. The ordering of function applications then becomes an issue, with Core Aldwych able to model either the enforcement of an ordering or the retention of indeterminate ordering, which allows parallel execution.
◦ 17:15-17:45: Verifying Unix-style utilities in CakeML
Scott Owens, University of Kent
CakeML is an impure functional programming language aimed at supporting formally verified programs. The CakeML project has several aspects including formal semantics and metatheory, a verified compiler, a mechanised connection between its semantics and higher-order logic (in the HOL4 interactive theorem prover), and an example verified theorem prover written in CakeML and HOL4. It also has respectable performance compared to industrial-strength implementations of ML.
The CakeML project has been running for five years and has achieved its initial goal of demonstrating the feasibility of a practical, mechanically verified compiler from program source text to target machine code. But where should we go from here? In this talk, I will present a nascent project on verifying core UNIX utilities, focussing on sort and grep. These examples are interesting because they interact with the outside world and perform pure computation. I will explain how we combine two different techniques to verify these programs: Arthur Charguéraud's characteristic formulae, and our own proof-producing translation from HOL to CakeML.[>
The costs of organising S-REPLS 6 were generously supported by ARM.
General information about S-REPLS can be found on the following page:
All S-REPLS related communications are made via the mailing list: http://www.jiscmail.ac.uk/srepls. This mailing list has very low traffic. If you have professional interests in programming language in the region, we encourage you to sign up.
Organising future meetings
If you would like to organise future meetings at your university or company, please get in touch with the steering committee: