Scottish Programming Languages Seminar

Monday 17th June 2019

The Scottish Programming Languages Seminar (SPLS) is an informal meeting for the discussion of any aspect of programming languages. SPLS will be held at the Informatics Forum, the University of Edinburgh on Monday 17th June 2019.

Information and updates about the June 2019 edition of SPLS will be communicated via the SPLS Mailing List.

Programme

The meeting will begin at 11:30 and last until 17:30. The talks will take place in room G.07.

11:30 — 12:30: Type-driven Verification and Weak Memory Semantics

Adam Barwell, Type-Driven Verification of Non-functional Properties
Energy, Time and Security (ETS) properties of programs are becoming increasingly prioritised by developers, especially where applications are running on ETS sensitive systems, such as embedded devices or the Internet of Things. Moreover, developers currently lack tools and language properties to allow them to reason about ETS. In this paper, we introduce a new contract specification framework, called Drive, which allows a developer to reason about ETS or other non-functional properties of their programs as first-class properties of the language. Furthermore, we introduce a contract specification language, allowing developers to reason about these first-class ETS properties by expressing contracts that are proved correct by an underlying formal type system. Finally, we show our contract framework over a number of representable examples, demonstrating provable worst-case ETS properties.
Ben Simner, Modelling instruction fetching in ARM assembly
Weak memory semantics studies modern hardware, such as ARMv8, which allow surprising behaviours. In this talk, I will give a brief introduction to this area and explain the ongoing work in modelling the system-level aspects of the Arm architecture as used in operating system kernels, and JIT compilers, particularly those related to self-modifying code. I will: show examples of weak behaviours for self-modifying code and instruction fetching; and give the current operational model that explains these behaviours. This work is used by architects to rigorously analyse their architecture, OS kernel programmers to gain confidence in the architectural guarantees for the correctness of their code, and programming language implementors who wish to implement efficient just-in-time compilation.

12:30 — 13:30: Lunch

Lunch will be served in the cafe area in the atrium.

13:30 — 14:30: Linearity and Strings

James Wood, Linear metatheory via linear algebra
It is well known that linear logic has semantics in symmetric monoidal closed categories, including the category of vector spaces and matrices. We find that, aside from semantics, vectors and matrices are useful in the syntax too. I will present a calculus related to Atkey's Quantitative Type Theory where usage of variables can be constrained in various ways via annotations on variables in the context. We read a context's worth of annotations as a vector, and get that substitution involves matrix-vector multiplication. This leads to a clean statement and proof of the substitution lemma, where the data stay the same even as usage restrictions change in the typing derivation.
Chad Nester, String Diagrams for Cartesian Restriction Categories
Partial maps occur violently in the foundations of computer science, so we should be interested in how partiality works. Restriction categories capture partiality abstractly, but the resulting formalism can be difficult to work with. String diagrams are becoming widely used as a tool to simplify the presentation of tedious proofs in settings where they apply. In this talk I will present a series of happy coincidences of structure that allow us to reason about restriction categories with restriction products (and more) using string diagrams.

14:30 — 15:00: Coffee break

Coffee, tea, and biscuits will be served in the cafe area in the atrium.

15:00 — 16:00: Probabilistic Programming and Deep Learning

Maria Gorinova, Program transformations for efficient probabilistic programming with discrete variables
The goal of probabilistic programming is to allow users to directly reason about their probabilistic models and processes generating data, while abstracting away the complicated algorithms needed to perform Bayesian inference. In practice, however, probabilistic programming languages are forced to trade off between generality of the language and efficiency of inference. For example, Stan — a popular probabilistic programming language — sacrifices discrete model parameters support, in exchange for efficient, gradient-based inference.

However, there exist work-around methods for inference with discrete parameters, as described by Stan's language manual. A knowledgeable and experienced user can manually encode discrete parameters into the program, by marginalising them out of the target probability density. In this work-in-progress talk, I will explain in more detail how this is achieved, and talk about possible ways of automating this process using program transformations.
José Cano Reyes, Moving Deep Learning to the Edge
In this talk I'll motivate the need for moving the execution of emerging deep learning applications to edge devices and I'll describe my recent work related to it. Finally, I'll outline some research ideas for future work.

16:00 — 16:30: Coffee break

Coffee, tea, and biscuits will be served in the cafe area in the atrium.

16:30 — 17:30: Dependent Types

Guillaume Allais, Generic Level Polymorphic N-ary Functions
Agda's standard library struggles in various places with n-ary functions and relations. It introduces congruence and substitution operators for functions of arities one and two, and provides users with convenient combinators for manipulating indexed families of arity exactly one.

After a careful analysis of the kinds of problems the unifier can easily solve, we design a unifier-friendly representation of n-ary functions. This allows us to write generic programs acting on n-ary functions which automatically reconstruct the representation of their inputs' types by unification. In particular, we can define fully level polymorphic n-ary versions of congruence, substitution and the combinators for indexed families, all requiring minimal user input.
Edwin Brady, Type Driven Development of Idris 2

17:30 — : Pub

Location

SPLS will take place at the Informatics Forum, 10 Crichton Street, Edinburgh. The main entrance is opposite Appleton Tower. The seminar will take place in room G.07. Lunch and coffee breaks will take place in the Atrium. All will be signposted on the day.

Further information about travelling to the Informatics Forum can be found on the School of Informatics web site.