Programming Languages
We present the first formalization and metatheory of language soundness for a user-schedulable language, the widely used array processing language Halide. User-schedulable languages strike a balance between abstraction and control in…
Hypersafety properties of arity $n$ are program properties that relate $n$ traces of a program (or, more generally, traces of $n$ programs). Classic examples include determinism, idempotence, and associativity. A number of relational…
Parallelism is often required for performance. In these situations an excess of non-determinism is harmful as it means the program can have several different behaviours or even different results. Even in domains such as high-performance…
This paper presents a proof system for reasoning about execution time bounds for a core imperative programming language. Proof systems are defined for three different scenarios: approximations of the worst-case execution time, exact time…
The monadic shallow linear (MSL) class is a decidable fragment of first-order Horn clauses that was discovered and rediscovered around the turn of the century, with applications in static analysis and verification. We propose a new class of…
We present Scrybe, an example-based synthesis tool for a statically-typed functional programming language, which combines top-down deductive reasoning in the style of $\lambda^2$ with Smyth-style live bidirectional evaluation. During…
Static information flow control (IFC) systems provide the ability to restrict data flows within a program, enabling vulnerable functionality or confidential data to be statically isolated from unsecured data or program logic. Despite the…
In scientific and engineering applications, physical quantities embodied as units of measurement (UoM) are frequently used. The loss of the Mars climate orbiter, attributed to a confusion between the metric and imperial unit systems,…
As the hardware industry moves towards using specialized heterogeneous many-cores to avoid the effects of the power wall, software developers are finding it hard to deal with the complexity of these systems. This article shares our…
We present a simple technique for semantic, open logical relations arguments about languages with recursive types, which, as we show, follows from a principled foundation in categorical semantics. We demonstrate how it can be used to give a…
Program sensitivity measures how robust a program is to small changes in its input, and is a fundamental notion in domains ranging from differential privacy to cyber-physical systems. A natural way to formalize program sensitivity is in…
Modern applications often manage time-varying data. Despite decades of research on temporal databases, which culminated in the addition of temporal data operations into the SQL:2011 standard, temporal data query and manipulation operations…
The calculus of constructions (CC) is a core theory for dependently typed programming and higher-order constructive logic. Originally introduced in Coquand's 1985 thesis, CC has inspired 25 years of research in programming languages and…
Elegant Objects (EO) is a programming language based on ideas of pure objects and the Decorator pattern. Bugayenko has suggested it as an intermediate representation for object-oriented programs. This paper presents a version of dynamic…
To warrant programmer productivity, type checker results should be correct and available quickly. Correctness can be provided when a type checker implementation corresponds to a declarative type system specification. Statix is a type system…
We present a new domain-agnostic synthesis technique for generating programs from input-output examples. Our method, called metric program synthesis, relaxes the well-known observational equivalence idea (used widely in bottom-up…
Pandemic management requires that scientists rapidly formulate and analyze epidemiological models in order to forecast the spread of disease and the effects of mitigation strategies. Scientists must modify existing models and create novel…
Genetic Programming (GP) is an heuristic method that can be applied to many Machine Learning, Optimization and Engineering problems. In particular, it has been widely used in Software Engineering for Test-case generation, Program Synthesis…
Correctly manipulating program terms in a compiler is surprisingly difficult because of the need to avoid name capture. The rapier from "Secrets of the Glasgow Haskell Compiler inliner" is a cutting-edge technique for fast, stateless…
Go is a popular statically-typed industrial programming language. To aid the type safe reuse of code, the recent Go release (Go 1.18) published on 15th March 2022 includes bounded parametric polymorphism via generic types. Go 1.18…