SPLS

The Scottish Programming Languages Seminar is an informal meeting for the discussion of any aspect of programming languages. SPLS will be held at the Informatics Forum, University of Edinburgh on Wednesday 11th October.

Information and updates about the October edition of SPLS will be sent via the SPLS Mailing List.

If you plan on attending, please register here so we have an idea of numbers for catering. There will be a vegetarian option available, but please let us know if you have any other dietary requirements.

We gratefully acknowledge the continued support of the SICSA Theory, Modelling and Computation theme.

Confirmed Speakers

• Adam Barwell (University of St Andrews) -- In Search of a Map
• James Chapman (University of Strathclyde) -- Delayed NBE
• Stuart Gale (University of Strathclyde) -- Normalization or Bust
• Jan de Muijnck-Hughes (University of Glasgow) -- Designing Hardware using Session Types and Dependent Types: A First Look
• Alastair Murray (Codeplay) -- Layering Abstractions: Heterogeneous Programming and Performance Portability
• Shayan Najd (University of Edinburgh) -- Embedding by Normalisation
• Chris Schwaab (University of St Andrews) -- First class Time and Energy for Multicore Systems
• Thomas Weber (Augsburg University / LMU Munich / TU Munich / University of Edinburgh) -- Building useful UIs using Uselets

Programme

The meeting will begin at 12:00 and last until 18:00. We will go for dinner at Pizza Posto at 7PM after the meeting, which is a nice pizza restaurant close to the Informatics Forum. We will confirm numbers on the day.

12:00 - 13:00: Lunch

13:00 - 14:00: Concurrency Session The

• 13:00 - 13:30: Jan de Muijnck-Hughes -- Designing Hardware using Session Types and Dependent Types: A First Look

  The Border Patrol Project seeks to investigate how state-of-the-art advances in programming language theory can provide better guarantees towards System-On-Chip (SoC) design and execution. Specifically we are interested in extending existing work on structural type systems for SoC with that of Multi-Party Session Types and Dependent Types.

  In this talk I will: briefly discuss the goals of the Border Patrol Project; outline some of the design challenges we have encountered so far when looking to adapt multi-party session types for describing hardware; and demonstrate how dependent types help reason about the structure of SoC architectures.

• 13:30 - 14:00: Thomas Weber -- Building useful UIs using Uselets

  Whenever we want to write an application for real-world users, some form of UI is required. But with something as unpredictable as a human on one side and a, usually non-trivial, application on the other, things are bound to get complicated. The fact that creating and updating UIs is often a boilerplate-heavy process doesn't help, either.

  That makes UIs not a lot of fun to write, hard to understand, and cumbersome to maintain.

  Splitting the UI into smaller components, a popular approach, helps with the development of the individual components but adds additional wiring-overhead.

  We will take a look at how concurrency models can give us a high level abstraction for easily composable UI components while allowing developers to focus on the parts of a UI that really matter.

14:00 - 14:30: Coffee

14:30 - 16:00: The Normali{s, z}ing Session

• 14:30 - 15:00: Stuart Gale -- Normalization or Bust

  This talk reports on the experiment of combining bidirectional typechecking with a small step operational semantics. Simply typed lambda calculus is, unsurprisingly, still normalizing. However, this is true even for terms that do not typecheck! The bidirectional setup marks each redex with its active type and reduction will get stuck if the type is insufficient.

• 15:00 - 15:30: Shayan Najd -- Embedding by Normalisation

  In this talk, I present the insight that the practical concept of embedded domain-specific compilers (EDSC), describing embedded domain-specific languages (EDSL) used for generating code often for external targets, is deeply related to the theoretical concept of Normalisation-By-Evaluation (NBE), describing the process of deriving the canonical form of terms with respect to an equational theory.

  Since an embedded term is encoded as a collection of host language terms, evaluation of the non-value host terms results in normalisation of the embedded term, and since EDSCs rely on an intermediate interface to generate their target code from, all embedded terms are designed to eventually adhere to the normal forms described by the interface. In other words, the structure of an EDSC allows it to perform Normalisation on embedded terms By encoding them as a collection of value and non-value host terms, employing Evaluation in the host language, and then deriving the resulting terms adhering to the intermediate interface. This structure, together with a collection of correctness laws, forms an NBE process.

  This connection, referred to as embedding by normalisation (EBN), is theoretically useful in that it helps us to understand and reason about embedded terms and their semantics, and practically beneficial in that it enables us to directly apply techniques from NBE. For instance, through EBN, we can adapt the treatment of sums, or constants, from NBE to embedding, resolving some not fully resolved problems.

• 15:30 - 16:00: James Chapman -- Delayed NBE

  This talk is about normalization by evaluation for simply typed lambda calculus using the delay monad. We use a novel coinductive approach to proving termination of the algorithm that initially requires only productivity. This allows the proofs of soundness and completeness that would otherwise be dependent on termination to be independent. In more complex situations where termination is difficult to prove or of lower importance this is a useful technique.

16:00 - 16:30: Coffee

16:30 - 18:00: The Parallel Session

• 16:30 - 17:00: Adam Barwell -- In Search of a Map

  Recursion schemes, such as the well-known map, can be used as loci of potential parallelism, where schemes are replaced with an equivalent parallel implementation. This talk describes a novel technique, using program slicing, that automatically and statically identifies computations in recursive functions that can be lifted out of the function and then potentially performed in parallel. We have implemented our approach, and will report on our results from applying our prototype to 12 Haskell examples, including benchmarks from the NoFib suite and functions from the standard Haskell Prelude.

• 17:00 - 17:30: Alastair Murray -- Layering Abstractions: Heterogeneous Programming and Performance Portability

  Widely used heterogeneous programming models such as OpenCL and CUDA provide programmers a means of exploiting heterogeneous hardware to achieve higher performance. A modern heterogeneous programming model, however, should also aid programmer productivity and allow for portable performance. This talk will give an overview of how this is being achieved by layering abstractions, by providing high-level domain specific approaches for programmers to model problems, and allowing the flexibility for even lower level layers to gain more precise control over hardware.

• 17:30 - 18:00: Chris Schwaab -- First class Time and Energy for Multicore Systems

  Verifying non-functional properties of programs, such as time and/or energy consumption, is often a difficult task. With emerging applications such as the internet-of-things, however, it is becoming increasingly important that devices operate reliably within known time and energy bounds. At the same time, processor architectures are becoming more complex. This means that traditional, usually compositional, modeling techniques are not effective. To solve this problem, we propose the introduction of fuzzy bounds that will allow us to reason formally about the probabilistic consumption of resources, in terms of program inputs. Our approach is type-directed, relating program sources directly to their probabilistic costs.

Venue and Travel

SPLS will take place at the Informatics Forum, 10 Crichton Street, Edinburgh. The main entrance is opposite Appleton Tower. The seminar will take place in rooms 4.31 / 4.33, and lunch and coffee breaks will take place in Mini Forum 1. All will be signposted on the day.

Further information about travelling to the Informatics Forum can be found on the School of Informatics web site.

Organisers

The organisers are Simon Fowler (simon.fowler -at- ed.ac.uk) and Craig McLaughlin (craig.mclaughlin -at - ed.ac.uk).