S-REPLS 14

Overview

S-REPLS is a series of informal meetings for people in the South of England interested in the principles, design and implementation of programming languages. Events take place approximately thrice yearly, organised by members of the community.

Date and location

  2 & A Half Devonshire Square
  Premier Place
  London
  EC2M 4UJ

organised by Leo White and Jeremy Yallop.

Registration

Schedule

0900-1000 Arrival and breakfast

 

1000-1100 Keynote: Graded types and Algebraic Effects
Dominic Orchard (University of Kent and University of Cambridge)

Graded types provide a means for fine-grained reasoning by reflecting the structure of typing rules into a system of type annotations. Graded modal types capture these annotations via indexed families of modalities whose indices have structure reflecting their operations. I'll give an overview of a few flavours and styles of grading in our research language Granule: a functional programming language resembling Haskell which combines indexed, linear, and graded types. I'll then show how we can leverage graded coeffect and graded effect types to give strong specifications for algebraic effects and handlers. Along the way, I'll brief signpost various related recent works from my group including graded types for uniqueness and borrowing and graded types for synthesis

1100-1130 Break

 

1130-1200 Automatically Finding Upper and Lower Time Complexity Bounds for Parallel Evaluation
Carsten Fuhs (Birkbeck, University of London)

In this talk, we revisit max-parallel-innermost term rewriting as a model of parallel computation on inductive data structures and provide a corresponding notion of runtime complexity parametric in the size of the start term. We propose automatic techniques to derive both upper and lower bounds on parallel complexity of rewriting that enable a direct reuse of existing techniques for sequential complexity. The applicability and the precision of the method are demonstrated by the relatively light effort in extending the program analysis tool AProVE and by experiments on numerous benchmarks from the literature.

This talk is based on joint work with Thaïs Baudon and Laure Gonnord.

1200-1230 Somewhat Dynamic Build Systems
Neil Mitchell (Meta)

The classic model of a build system, as presented in Build Systems a la Carte, is a single dependency graph. But in practice, large-scale build systems such as Bazel and Buck2 have two main dependency graphs - a target graph, and an action graph which refines the target graph. Both graphs can vary on the static vs dynamic spectrum (or alternatively, applicative vs monadic), giving either increased analysability or increased expressiveness.

In this talk we'll show the analysability requirements necessary to implement an efficient system to test the modified subset of a project. We'll also show the expressiveness requirements necessary to implement various language rules including Python, OCaml and Haskell. We then show how making the graphs dynamic in just the right ways gives us both, and have implemented these features in the Buck2 build system.

1230-1330 Lunch

 

1330-1400 The Dafny Programming Language and Static Verifier
Stefan Zetzsche (Amazon)

In this talk, I will give an overview of Dafny, a verification-aware programming language that is actively used within Amazon, and also heavily contributed to by Amazon.

Dafny is a full-grown language with support for common programming concepts such as inductive datatypes, lambda expressions, and classes. It can be compiled to C#, Java, Javascript, Python, and Go, making integration with existing workflow possible.

At the same time, Dafny offers an extensive toolbox for mathematical proofs about programs, including quantifiers, (co-)induction, and the ability to use and prove lemmas. Programs can be annotated in the style of Hoare-Logic, with pre-and post-conditions, loop-invariants, as well as termination and read/write framing specifications. Proofs can be verified instantaneously, through compilation to the Boogie intermediate language, which uses the Z3 SMT solver to discharge proof obligations.

After an initial introduction, I’ll give a live-demo of Dafny. I’ll then review some of its recent use cases in industry and academia, and highlight its potential for supporting your own research.

1400-1430 Implementing a Dependently Typed Language Modelling Algebraic Equivalences
Zhiyi Liu (University of Cambridge)

In a dependently typed language, types may contain arbitrary expressions as indices. Hence, deciding term equality is crucial in type conversion checks. The type checker can usually automate term equality judgements when one term reduces to the other through evaluation; otherwise, explicit identity proofs are required. For instance, to prove the equivalence between Vec x and Vec (x + 0), since (x + 0) is a neutral term and does not reduce to x, the user must supply proof for (x + 0 = x) so that the indices could be equated.

The problem boils down to the treatment of partially static terms, i.e. terms containing both constants and variables. Free extension (frex) is a universal framework proposed by Yallop et al. (2018) to view partially static terms as free extensions of algebra. With a suitable semantic domain, frex allows the representations of partially static terms to model equational theories, such as the identity properties of 0 in additive natural numbers.

In this talk, I will present a toy dependently typed language implemented with Normalisation by Evaluation (NbE) with free extensions on first-order neutral terms of various data types, as proposed by Corbyn et al. (2022). The type checker can generate normal forms in the context of relevant equational theories, automating conversion checks up to respective algebraic equivalences.

1430-1500 Programming with First-class Constructor Contexts
Anton Lorenzen (University of Edinburgh)

Constructor contexts are a new representation for data structures with a hole. Unlike zippers, they do not reverse the path from the hole to the root and instead just keep a mutable reference to the hole. In this talk, I show how they can be used to implement tail recursion modulo cons; even in tricky cases, such as for the partition and flatten functions, mutual recursion and polymorphic recursion. Furthermore, they are first-class values, which makes it possible to use them as efficient difference lists. Constructor contexts can be implemented in any language, with either uniqueness types/modes, reference counting, or a garbage collector.

1500-1530 Break

 

1530-1600 Finding cheaper straightline instruction sequences more cheaply
Maria A Schett

Based on Unbounded Superoptimization by Greta Yorsh (Jane Street, Onward!17), we developed the bytecode superoptimizer ebso to optimize straightline instruction sequences of Ethereum bytecode (presented at LOPSTR19 and 11th S-REPLS). But running ebso was very expensive, so this talk is about how we made our findings practical. We took two directions:

1. automatically generating peephole optimzation rules (FMBC20)
2. an encoding of stack operations together with symbolic execution using max SMT (CAV2020).

I'll also talk about our tools (in OCaml) and evaluation on 100 000+ real-world contracts.

1600-1630 Starlark: between configuration and programming language
Stiopa Koltsov (Meta)

In Meta we develop starlark-rust, a Starlark language implementation in Rust.

Starlark is an embeddable Python-like programming language occupying a niche between programming, scripting and configuration languages. It offers familiar syntax, and deterministic, isolated evaluation, which is a strict requirement for large build systems, which are historically primary users of Starlark (including Meta's Buck build system or Google's Bazel). But it is not limited to that.

This talk is about how Starlark is used or can be used, and what interesting features it offers.

1630-1700 Ill-Typed programs don’t evaluate
Charlie Walpole (University of Bristol)

We introduce two-sided type systems, which are sequent calculi for typing formulas. Two-sided type systems allow for hypothetical reasoning over the typing of compound program expressions, and the refutation of typing formulas. By incorporating a type of all values, these type systems support more refined notions of well-typing and ill-typing, guaranteeing both that well-typed programs don't go wrong and that ill-typed programs don't evaluate - that is, reach a value. This makes two-sided type systems suitable for incorrectness reasoning in higher-order program verification, which we illustrate through an application to precise data-flow typing in a language with constructors and pattern matching. Finally, we investigate the internalisation of the meta-level negation in the system as a complement operator on types. This motivates an alternative semantics for the typing judgement, which guarantees that ill-typed programs don't evaluate, but in which well-typed programs may yet go wrong.

Mailing list

If you would like to receive notifications of future meetings, please sign up to the (low-traffic) S-REPLS mailing list.

Questions

Please contact the organisers:

• Leo White (lwhite@janestreet.com)
• Jeremy Yallop (jeremy.yallop@cl.cam.ac.uk)