We will be physically located in 40 George Square, room LG.09 LG.11 at the University of Edinburgh.
To reach LG.11, please take the Windmill lane entrance, see the pin here.
Accessibility information is available here.
For online participants, we have sent a Zoom link via the SPLS mailing list and on the SPLS Zulip.
We are happy to announce that José Pedro Magalhães, a Managing Director at Standard Chartered Bank, will be giving the keynote.
José Pedro Magalhães is a Managing Director leading a team of ~45 quantitative developers at Standard Chartered Bank. He is also one of the founders of Chordify.
Before joining Standard Chartered, he was a postdoctoral research assistant in the Programming Languages group at the Department of Computer Science of the University of Oxford, working on the Unifying Theories of Generic Programming project.
Previously he was a PhD student at the Department of Information and Computing Sciences of Utrecht University in the Netherlands. His PhD topic was Real-Life Datatype Generic Programming, supervised by Johan Jeuring, Andres Löh, and Doaitse Swierstra. Before that he graduated from Minho University in Computer Science and Systems Engineering (Licenciatura em Engenharia de Sistemas e Informática).
He has also been a Summer Student at CERN, an intern at Philips Research, and a research intern at Microsoft Research Cambridge.
Registration
If you plan to attend in person register by the 19th June 2024 using this form.
If you wish to give a talk then please indicate it in the above form. If your title or abstract is yet to be determined, they can be sent by the 24th June 2024 per email to one of the organizers.
Registration is required for catering.
Programme
11:30—12:30 Session 1: Keynote
José Pedro Magalhães (Standard Chartered Bank)
Functional Programming in Financial Markets
In this talk we showcase the application of functional programming in a very large industrial setting. At Standard Chartered Bank, Haskell forms the core of a software library supporting the entire Financial Markets (FM), a business line with 5 billion USD operating income in 2023. Typed functional programming is used across the entire tech stack, including foundational APIs and CLIs for deal valuation and risk analysis, server-side components for long-running batches or sub-second RESTful services, and end-user GUIs. Thousands of users interact with software built using functional programming, and over one hundred write their own functional code.
We present the history of how functional programming established itself in FM, including the rationale for having our own compiler and dialect of Haskell. We then focus on how we leverage it to orchestrate type-driven large-scale pricing workflows. The same API can be used to price one trade locally, or millions of trades across thousands of nodes in the cloud. We build upon decades of research and experience in the functional programming community, relying on concepts such as monads, lenses, datatype generics, and closure serialisation.
12:30—13:30 Lunch (with coffee)
13:30—14:30 Session 2: Talks
Danielle Marshall (Glasgow and Kent)
Linearity, Uniqueness, Ownership: An Entente Cordiale
Substructural type systems, which restrict the use of weakening and contraction rules from intuitionistic logic, are growing in popularity because they allow for a resourceful interpretation of data which can be used to rule out software bugs. Substructurality is finally taking hold in practical programming: Haskell now has linear types based on Girard's linear logic but integrated via graded function arrows, Clean has uniqueness types ensuring that values have at most a single reference, and Rust has an intricate ownership system guaranteeing memory safety. But despite this broad range of resourceful type systems, there has been comparatively little work on understanding their relative strengths and weaknesses. We demonstrate how linear types and uniqueness types can be used within a single system in the setting of the Granule language to offer both restrictions on local program behaviour and guarantees about global memory usage. We then extend this framework further, by showing that just like graded type systems as in Granule or Idris build upon linearity, Rust's ownership model builds upon uniqueness. We develop an extended type system incorporating ownership and borrowing based on ideas from both fractional permissions and graded types, and implement this in Granule.
Bruce Collie (Runtime Verification, Inc.)
Meeting Developers Where They Are: Lessons Learned from Formal Verification in Practice
Most (if not all) attendees of this workshop will have some idea of the benefits of applying formal verification techniques to software: we can prove to ourselves and others that our code behaves properly, rather than simply asserting this claim by testing (or worse, asserting it without substantiation). However, in our experience, the average developer "on the street" is not aware of these benefits, and even if they are, they may lack the time, opportunity or masochism required to start applying academic tools to their code in practice.
This talk is a tour through some of the lessons we've learned trying to get developers on board with formal verification in practice. I'll cover the underlying PL semantics techniques we base our work on, then go through a few representative examples of how we've tried to make more accessible and applicable FV software by meeting users "where they are", all without compromising on the underlying rigour and power of the tools in question.
14:30—15:00 Break (with coffee)
15:00—16:00 Session 3: Talks
Robert Wright (Edinburgh)
First-class Algebraic Presentations with Elaborator Reflection
We present a library for the ergonomic creation, manipulation, and use of first-order algebras. We do not rely on hard-coded syntactic support for our embedded language. Instead, we use metaprogramming to provide syntactic sugar for creating and using user-definable deeply-embedded first-order algebras.
Jeremy Singer (Glasgow)
Haskell in High School: Functional Programming for School Age Learners
In conjunction with a colleague from Stanford University, we are deploying Haskell programming materials in Welsh high schools. The aim is to enable participants to create learning and teaching resources for algebra as part of work towards the Welsh Baccalaureate. In this short talk, I will review the Haskell materials used and consider the responses from early adopters. I will highlight challenges and opportunities related to teaching functional programming to younger learners.
16:00—16:30 Break (no coffee)
16:30—17:30 Session 4: Talks
Conor McBride (Strathclyde and Quantinuum)
Fulls Seldom Differ
One use for type-level numbers is to capture patterns of scaling up, e.g. "adding a pair of 2^n bit numbers and a carry-in to get a carry-out and a 2^n bit sum". These patterns often rely on reasoning steps such as "2^n is even iff n is a successor". We reach a place where type-level arithmetic is no longer enough. It's healthy to ask how the language of type-level numeric expressions impacts on the division of algebraic labour between programmer and typechecker. I'll present the current state of my enquiries, but the key observation is that (2^) is a troublesome primitive, but its neighbour, full(n) = (2^n)-1 (i.e., the n-bit number full of 1s) is remarkably cooperative. The numbers which happen to be the difference between two fulls have some rather special properties, yielding a carefully curated constraint space with a complete unification algorithm.
Dylan Thinnes (Digital Asset)
Structured Error Messages and Error Postprocessing in GHC
Error messages are tricky - they need to be approachable for new users, informative for experienced users, interact with complicated type system features, and diagnose problems with limited information. In this talk we briefly go over the many difficulties facing the would-be error generator, some peculiar use cases, and existing efforts in the Glasgow Haskell Compiler for enabling better error messages for everyone.
17:30—late Pub
Travel
The University of Edinburgh (Central Area) is located a short (fifteen minutes) walk from Edinburgh Waverley, heading south from the City Centre.
The University provides travel information including maps and directions.
Please take the Windmill lane entrance to access LG.09 LG.11, see the pin below.
Organised by Jesse Sigal, Brian Campbell, and Xueying Qin.
Should you have comments or queries about the event please contact one of the organisers by email <firstname DOT lastname AT ed DOT ac DOT uk> or on Zulip.
