Please register for the SPLS meeting here. The main purpose of the registration is to estimate the number of participants so that we could adjust the online platforms accordingly.
The meeting will be coordinated using the #spls-2021-06 stream on the SPLS Zulip chat service.
The talks will be delivered via Zoom. The talks will also be live-streamed to the SPLS youtube channel. .
The links to the Zoom meetings will be announced on Zulip prior to the talks.
Breaks and the virtual pub session will take place in the SPLS bar on gather.town. The link to the room will be posted on Zulip.
All the times below are given in UTC+01:00 (UK time zone).
13:00–14:00 |
Neel Krishnaswami
Adjoint Reactive GUI Programming
Most interaction with a computer is done via a graphical user interface. Traditionally, these are implemented in an imperative fashion using shared mutable state and callbacks. This is efficient, but is also difficult to reason about and error prone. Functional Reactive Programming (FRP) provides an elegant alternative which allows GUIs to be designed in a declarative fashion. However, most FRP languages are synchronous and continually check for new data. This means that an FRP-style GUI will “wake up” on each program cycle. This is problematic for applications like text editors and browsers, where often nothing happens for extended periods of time, and we want the implementation to sleep until new data arrives. In this paper, we present an asynchronous FRP language for designing GUIs called λWidget. Our language provides a novel semantics for widgets, the building block of GUIs, which offers both a natural Curry–Howard logical interpretation and an efficient implementation strategy. |
14:15–14:45 |
Thomas Koehler
Optimizing Functional Programs with Equality Saturation
Equality saturation is a rewrite-driven optimization technique which leverages a special data structure called e-graph to efficiently represent many variants of a rewritten expressions. However, challenges arise when applying this technique to optimize functional programs. How can we for example efficiently implement alpha-equivalence; substitution for beta-reduction; or predicates for eta-reduction? In this talk, we investigate different solutions to address these challenges, such as using De-Bruijn indices instead of named identifiers. We show their impact in practice when optimizing programs expressed in Rise: a typed lambda calculus. We will show that the presented solutions enable us to discover more complex optimizations than a naive implementation, although scaling the technique further remains an open challenge. |
15:00–15:30 |
Jamie Gabbay
Nominal programming for the working programmer
I'll outline what it would take to implement a "Nominal" package in an arbitrary programming language, generalising from my experience from designing the Nominal Haskell package. |
16:00–16:30 |
Sam Lindley
Handler calculus
We present handler calculus, a core calculus of effect handlers. Inspired by the Frank programming language, handler calculus does not have primitive functions, just handlers. Functions, products, sums, and inductive types, are all encodable in handler calculus. We extend handler calculus with recursive effects, which we use to encode recursive data types. We extend handler calculus with parametric operations, which we use to encode existential data types. We then briefly outline how one can encode universal data types by composing a CPS translation for parametric handler calculus into System F with Fujita’s CPS translation of System F into minimal existential logic. |
16:45–17:15 |
Wen Kokke
Prioritise the Best Variation
Binary session types guarantee communication safety and session
fidelity, but alone they cannot rule out deadlocks arising from the
interleaving of different sessions. |
17:30–18:00 |
Celeste Hollenbeck
Investigating Magic Numbers: An Evaluation of Inlining in the Glasgow Haskell Compiler
Haskell’s performance can sometimes rival that of low-level languages. However, many of the performance-affecting decisions of the Glasgow Haskell Compiler (GHC) are informed by out-of-date heuristics typically evaluated on nofib, an out-of-date benchmark suite. We investigated the case for upgrading GHC’s inliner by gathering performance data across real-world Haskell packages. To do so, we developed an updated benchmark suite and evaluated the impact of some of GHC's hard-coded constants, or "magic-numbers", on GHC’s inlining behaviour. Using these benchmarks, we demonstrated the potential for a 12.37 % geometric mean speedup. This speedup is not attainable, however, without rewriting GHC’s inliner. With its current code, our analysis shows that a replacement of the inliner’s numerical thresholds—its magic numbers—would only yield a speedup of 5.36%, justifying a rethink of GHC’s inliner design. |
19:00–... | Virtual Pub |