Wednesday March 13th 2019, 12noon - 5:30pm
Lunch: School of Computer Science, University of St Andrews, KY16 9SX (map, directions) thanks to SICSA.
Talks: Maths Lecture Theatre B
12noon | Lunch | ||
12:45pm |
Bastian Hagedorn (University of Münster) | Elevate: A language for expressing optimisation strategies | |
1:15pm |
Sam Lindley
(University of Edinburgh) | On the relative expressive power of equi-recursive and iso-recursive types | |
1:45pm |
Bob Atkey (Strathclyde University) | One Monad to the Tune of Another | |
2:15pm | Coffee | ||
2:45pm |
Ekaterina Komendantskaya (Heriot-Watt University) | SICSA Summer School on Verification and Programming Languages (Slides) | |
3:00pm |
Philippa Cowderoy | Information-Aware Type Systems (Slides) | |
3:30pm |
Malin Altenmuller (Strathclyde University) | Containers of Applications and Applications of Containers | |
4pm | Coffee | ||
4:30pm |
Ohad Kammar (University of Edinburgh) | Eff-Bayes: modular implementations of approximate Bayesian inference with effect handlers | |
5:00pm |
Conor McBride (Strathclyde University) | Type Theory: Rules OK? | |
5:30pm | Pub and dinner |
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)
Abstract to follow
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.
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.
Abstract to follow
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.
Abstract to follow
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!
General information about SPLS is available from the SPLS page. For information about the event, please contact the organiser:
SPLS receives financial support from SICSA, the Scottish Informatics and Computer Science Alliance.