SPLS October 2019 in Glasgow

The Scottish Programming Languages Seminar (SPLS) is an open forum for researchers interested in programming languages. Held every few months, the first meeting of the 2019/20 season will be in the:

School of Computing Science


University of Glasgow


[2019-10-30 Wed 12:00-17:30]

The programme for the meeting will be detailed below with more information being published via the SPLS Mailing List.


We would like to acknowledge the continued support of SICSA, and especially SICSA's Theory, Modelling, and Computation Theme. We would also like to acknowledge the support of MaRIONet the UK Manycore Network for helping to fund this edition of SPLS.


While attendance at SPLS is free, we would appreciate if you can register here so that we can have a better idea of numbers for catering. A vegetarian option will be available but please do contact us if you have any other dietry requirements.


If you are interested in giving a talk please fill out the form:


Like previous SPLS' before us we will prioritise talks about work-in-progress, and those from students and people new to the community.

We will confirm the speaker line up at least two weeks before on:

Monday 14th October, 2019.


1200-1245: Lunch
1245-1300: Opening Remarks & News
1300-1400: KeyNote: Prof. James Noble — Through a Glass, Darkly (John Disco remix)

Object-oriented programs are often described as "models of the real world". Drawing on the work of Peirce, Sassure, Peter Bogh Anderson, and H. P. Lovecraft, I'll try and explain what this means and how it affects our programs and programming languages — functional, object-oriented, chthonic, or otherwise. I'll look at the relationships between simulation, programming, meta-programming, delegation, and inheritance. I'll try and justify the de-evolution from SIMULA to Smalltalk, Self, and Javascript. Finally I'll speculate about what it means when our programs don't just simulate the real world, but rise from the abyss replace it.

1400-1430: Coffee Break
1430-1600: Session 0
1430-1500 Simon Fowler (University of Edinburgh) Model-View-Update-Communicate: Session Types meet the Elm Architecture.

The Elm programming language pioneers the Model-View-Update (MVU) architecture for writing web applications in a functional style. Although popular amongst developers, MVU has not been studied formally; it is therefore difficult to reason about any extensions, and each implementer must re-discover the essence of the architecture.

We introduce lambda-mvu, a formal description of the MVU architecture as a concurrent lambda-calculus, and prove its correctness. We modularly extend lambda-mvu with subscriptions and commands as found in the Elm programming language. We then further extend the calculus with linearity and model transitions, which are sufficient to allow us to provide the first formal integration of session-typed communication in a GUI framework. We implement our approach in the Links tierless web programming language, and show examples including a two-factor authentication workflow and multi-room chat server.

1500-1530 Jeremy Singer (University of Glasgow) Language Interoperability Patterns in Jupyter Notebooks.

Here are two trending topics in contemporary software development:

  1. interactive notebook coding, e.g. Jupyter notebooks
  2. multi-language projects, i.e. polyglot programming

This presentation examines the crossover between these two topics, and identifies a set of architectural design patterns that facilitate differing levels of programming language interoperability in such interactive environments. Health warning - this is work-in-progress ... or maybe work-about-to-start (?)

1530-1600 Philippa Cowderoy Telescopic Constraint Trees.

Telescopes give us composable contexts, but what if we could compose them more than one way?

I tried it, coupled it with an Information Aware presentation of type systems, and found a useful collection of tools to share. In particular, I derived a new representation for solving typechecking problems and a way to proceed from a type system to a logical specification of existing techniques suitable for checking dependently typed languages.

Aside from reading off implementations and verifying more complex ones, I hope this representation can also be used to discuss nuanced differences between systems and to explain the behaviour of typecheckers to users.


1600-1630: Coffee Break
1630-1730: Session 1
1630-1700 Artjoms Šinkarovs (Heriot-Watt University) Making Sense of APL using Dependent Types.

Multi-dimensional arrays play a major role in machine learning, numerical simulations or high-performance computing. Array programming in imperative languages involves explicit indexing within loop-nests which often leads to the code that is difficult to understand or reason about. APL offers a notation for array operations that is built around the notion of index-free combinators. APL programs are very concise yet carry very rich semantics. However, as APL is dynamically typed, reasoning about correctness of these programs is challenging.

Designing a type system for APL is even more challenging. First, the same operator has different behavior depending on the type and shape of its arguments. Secondly, the shape of the result of an operator typically depends on the shape of its arguments. Finally, the type of array elements may change at runtime.

In this talk I will describe preliminary results on formalising APL in Agda. I will present a shallow embedding of a core array language that makes it possible to define a set of APL operators and partially solve the overloading. As a result, a large set of APL programs can be translated into the proposed system. They can be then analysed for correctness or interpreted within Agda or compiled into executables.

1700-1730 James Wood (University of Strathclyde) A Bool in the Hand is Worth Two in the Bush.

A common practice in dependently typed programming is correct-by-construction programming — where we write programs that carry statically a lot of the information that is needed to verify them. For example, instead of having filter take a list of XS and produce a list of XS, we declare a property P and return, as well as the list of XS, a proof for each x in the returned list that it satisfies P. However, when we do correct-by-construction programming with fancy types, we sometimes lose sight of how these functions compute. In this talk, I rectify a long-standing bug in the Agda and Idris standard libraries in their definitions of Dec — the type family that captures the decidability of a proposition — so as to get back good computational properties.

1730+ Pub/Dinner

Venue & Travel

The event will be held within:

SAWB 422/23, School of Computing Science, University of Glasgow

Directions are available.


If you have any questions please contact: