South of England Regional Programming Language Seminar (S-REPLS)
S-REPLS is a regular and informal meeting for those based in the South of England with a professional interest—whether it be academic or commercial—in the semantics and implementation of programming languages. S-REPLS 2 will take place at Middlesex University London, on Friday, 20th November 2015. It will follow the successful low-overhead formula of the previous meeting at Cambridge: a “pop-up” meeting, if you like. For this edition, we are delighted to have Nick Benton, Paul Kelly, Sam Staton and Phil Wadler as invited speakers. The tentative schedule is as follows, where you can click on the talk title to see the abstract:
- 11:45–12:00, Arrival
- 12:00–12:45, Invited Talk: Nick Benton (Microsoft Research, Cambridge)
What We Talk About When We Talk About Types
Types are a central topic in programming language research, as well as being a major trigger of heated and unproductive language advocacy arguments on the internet. Yet, even amongst expert types researchers, there is a surprising diversity of opinion about just what types are: what they mean, what they’re for, and what properties a type system should have. This talk will explore the various positions, including, of course, presenting the correct answers to these questions.
- 12:50–14:00, Lunch
- 14:00–14:45, Invited Talk: Phil Wadler (Edinburgh)
Everything old is new again: Quoted domain specific languages
Fashions come, go, return. We describe a new approach to domain specific languages, called QDSL, that resurrects two old ideas: quoted terms for domain specific languages, from McCarthy’s Lisp of 1960, and the subformula property, from Gentzen’s natural deduction of 1935. Quoted terms allow the domain specific language to share the syntax and type system of the host language. Normalising quoted terms ensures the subformula property, which provides strong guarantees, e.g., that one can use higher-order or nested code in the source while guaranteeing first-order or flat code in the target, or using types guide loop fusion. We give three examples of QDSL: QFeldspar (a variant of Feldsar), P-LINQ for F\#, and some uses of Scala LMS; and we provide a comparison between QDSL and EDSL (embedded DSL).
[Joint work with James Cheney, Sam Lindley, Shayan Najd, and Josef Svenningsson.]
- 14:50–15:20, Coffee/Tea Break
- 15:20–15:40, Contributed Talk: Richard Bornat (Middlesex)
Lace: a program logic for weak memory
Weak memory reorders instruction execution and propagation of writes to the store. It’s hard to understand and harder still to program. We have a program logic based on Hoare logic, Owicki-Gries and Jones’s rely/guarantee, which makes programming easier and proof possible.
[Joint work with Jade Alglave and Matthew Parkinson]
- 15:40–16:25, Invited Talk: Paul Kelly (Imperial)
How does domain specificity enable domain-specific performance optimisations?
My group at Imperial has worked on six or seven “domain-specific optimisation” (DSO) projects, mostly in computational science applications. This talk aims to reflect on our experiences, and in particular, to ask what enables us to deliver a DSO? Is it some special semantic property deriving from the domain? Is it because we have a domain-specific language that abstracts from implementation details – enabling the compiler to make choices that would be committed in lower-level code? Is it that the DSL captures large-scale dataflows that are obscured when coded in a conventional general-purpose language? Is it simply that we know that particular optimisations are good for a particular context? The talk will explore this question with reference to our DSO projects in finite-element methods, unstructured meshes, linear algebra and Fourier interpolation.
[This is joint work with many collaborators.]
- 16:25–16:45, Coffee/Tea Break
- 16:45–17:30, Invited Talk: Sam Staton (Oxford)
Equations, effects and resources
I will discuss equational theories of programming languages. I’ll focus on first order languages that use some kind of resource. I’ll take illustrations from quantum computation, where the resource is “qubits”. The development is based around an equivalence between first-order programming languages and algebraic theories, as I’ll explain.
- 17:30–17:50, Contributed Talk: John Wickerson (Imperial)
Overhauling SC atomics in C11 and OpenCL
In this talk, I will outline our proposal for overhauling the semantics of SC atomics in C11 and OpenCL. In the C11 case, I will describe a revised model that is shorter, simpler, and demonstrably more efficient to simulate. Our revised model is a little stronger than the current one (i.e., allows fewer program behaviours) but existing compilation schemes (Power, x86) remain sound. I will then describe how we have extended our revised C11 model to obtain the first rigorous formalisation of the OpenCL memory model. (OpenCL is an extension of C for heterogeneous programming across CPUs, GPUs, FPGAs, etc.) In the OpenCL case, we refine the SC rules still further, to give a sensible semantics to SC atomics that employ a ‘memory scope’ to restrict their visibility to specific threads.
[This is joint work with Mark Batty and Ally Donaldson, and will be presented at POPL 2016.]
The meeting will start at 12:00, with lunch at 12:50 and the meeting will close around 18:00. There is no registration fee and lunch will be provided. The talks will take place in the Council Chamber, Hendon Town Hall, The Burroughs, Hendon, London NW4 4BT. Please sign in at the reception. The Hendon Campus is about a 10 minute walk (mostly uphill) from Hendon Central, which is 30 minutes from Central London on the tube (Northern Line, Edgware Branch). It is also well connected by buses and Thameslink, and is close to the southern end of the M1. Parking is scarce around the campus but there is free parking west of A41 (a 10 minute walk ) after 11 a.m. More information about the campus and getting to the university can be found here. The Transport for London website may also be useful.
Please email Andrei Popescu at a.popescu @ mdx.ac.uk if you are coming to S-REPLS. This will allow us to update the mailing list, and also ensure that we don’t run out of food at lunchtime.