Scottish Programming Languages Seminar

Bastian Hagedorn: Elevate: A language for expressing optimisation strategies

The increasing trend towards specialised hardware accelerators makes writing portable software that achieves high performance and efficiency across multiple devices a challenging – if not impossible – task for most programmers. Higher level programming languages combined with sophisticated code generators have emerged as a promising direction to address this performance portability challenge. Among these approaches is the Lift project (www.lift-projet.org). The high-level Lift language allows developers to express applications in a composable and portable way. Lift programs are then translated with a rewrite system into a low-level form from which high-performance code is generated. These two layers clearly separate the functional “what to compute” from the imperative “how to compute it”. In this talk I will present an early version of Elevate a new language to define optimisation strategies of Lift programs as compositions of rewrite rules. While other systems, such as Halide, provide means to apply schedules or strategies externally, Elevate is designed to be extensible and allows developers to define their own optimisation strategies such as tiling or particular strategies to map computations to the hardware. I will show that Lift and Elevate successfully address the performance portability challenge on a series of applications ranging from linear algebra over HPC stencil computations to machine learning.

This is joined work with Michel Steuwer (University of Glasgow)

Sam Lindley: On the relative expressive power of equi-recursive and iso-recursive types

Abstract to follow

Bob Atkey: One Monad to the Tune of Another

I'll talk about a generic way of reasoning about monadic computations by mapping one monad, the "computational" monad, to another, the "specification" monad via a monad morphism. Such monad morphisms allow us to reconstruct existing program logics for state, I/O, nondeterminism, and exceptions. Monad morphisms can be packaged up neatly as a "Dijkstra Monad" -- essentially a monad graded by another monad -- yielding a useful technique for simultaneous programming and verification.

This is joint work with Kenji Maillard, Danel Ahman, Guido Martínez, Cǎtǎlin Hriţcu, Exequiel Rivas and Éric Tanter.

Ohad Kammar: Eff-Bayes: modular implementations of approximate Bayesian inference with effect handlers

I will describe work-in-progress, implementing a library for Bayesian inference algorithms for statistical probabilistic programming in the programming language Eff using algebraic effects and handlers.

Joint work with Matija Pretnar, Žiga Lukšič, Oliver Goldstein, and Adam Ścibior.

Ekaterina Komendantskaya: SICSA Summer School on Verification and Programming Languages

Abstract to follow

Philippa Cowderoy: Information-Aware Type Systems

It's easy to get confused by what's going on in a modern type system. Whether we're doing metatheory and struggling to show something we hope is obvious, or just looking at part of a type error message and wondering "where's that from?!"

With a Simple and familiar example, I'll demonstrate how we can use a range of tools to make ourselves more aware of how information behaves in a type system. Information effects per James and Sabry enable a new presentation - and a path to information awareness.

Malin Altenmuller: Containers of Applications and Applications of Containers

Abstract to follow

Conor McBride: Type Theory: Rules OK?

How should we make sure that the rules of a type theory are ok, in the sense that they admit sensible metatheoretical properties, e.g. stability under substitution? By giving a type of ok typing rules, of course! Physician, heal thyself!

Contact