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.
The meeting will begin at 11:30 and last until 17:30. The talks will take place in room G.07.
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.
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.
Lunch will be served in the cafe area in the atrium.
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.
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.
Coffee, tea, and biscuits will be served in the cafe area in the atrium.
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.
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.
Coffee, tea, and biscuits will be served in the cafe area in the atrium.
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.
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.
Please register using the RSVP tool to indicate whether you like to attend the event. Registration is free and non-binding.
The organisers are Daniel Hillerström and Sam Lindley, contact us via e-mail ({first.lastname}@ed.ac.uk).