All Outputs (51)

Quotient Haskell: Lightweight Quotient Types for All (2024)
Journal Article

Subtypes and quotient types are dual type abstractions. However, while subtypes are widely used both explicitly and implicitly, quotient types have not seen much practical use outside of proof assistants. A key difficulty to wider adoption of quotie... Read More about Quotient Haskell: Lightweight Quotient Types for All.

Calculating Compilers for Concurrency (2023)
Journal Article

Choice trees have recently been introduced as a general structure for defining the semantics of programming languages with a wide variety of features and effects. In this article we focus on concurrent languages, and show how a codensity version of c... Read More about Calculating Compilers for Concurrency.

Monadic compiler calculation (functional pearl) (2022)
Journal Article

Bahr and Hutton recently developed a new approach to calculating correct compilers directly from specifications of their correctness. However, the methodology only considers converging behaviour of the source language, which means that the compiler c... Read More about Monadic compiler calculation (functional pearl).

Calculating dependently-typed compilers (functional pearl) (2021)
Journal Article

Compilers are difficult to write, and difficult to get right. Bahr and Hutton recently developed a new technique for calculating compilers directly from specifications of their correctness, which ensures that the resulting compilers are correct-by-co... Read More about Calculating dependently-typed compilers (functional pearl).

Calculating correct compilers II: Return of the register machines (2020)
Journal Article

In ‘Calculating Correct Compilers’ (Bahr & Hutton, 2015), we developed a new approach to calculating compilers directly from specifications of their correctness. Our approach only required elementary reasoning techniques and has been used to calculat... Read More about Calculating correct compilers II: Return of the register machines.

Liquidate your assets: reasoning about resource usage in liquid Haskell (2019)
Journal Article

Liquid Haskell is an extension to the type system of Haskell that supports formal reasoning about program correctness by encoding logical properties as refinement types. In this article, we show how Liquid Haskell can also be used to reason about pro... Read More about Liquidate your assets: reasoning about resource usage in liquid Haskell.

Call-by-need is clairvoyant call-by-value (2019)
Journal Article

Call-by-need evaluation, also known as lazy evaluation, provides two key benefits: compositional programming and infinite data. The standard semantics for laziness is Launchbury’s natural semantics, which uses a heap to memoise the results of delayed... Read More about Call-by-need is clairvoyant call-by-value.

AutoBench: comparing the time performance of Haskell programs (2018)
Conference Proceeding

Two fundamental goals in programming are correctness (producing the right results) and efficiency (using as few resources as possible). Property-based testing tools such as QuickCheck provide a lightweight means to check the correctness of Haskell pr... Read More about AutoBench: comparing the time performance of Haskell programs.

Theorem proving for all: equational reasoning in Liquid Haskell (Functional Pearl) (2018)
Conference Proceeding

Equational reasoning is one of the key features of pure functional languages such as Haskell. To date, however, such reasoning always took place externally to Haskell, either manually on paper, or mechanised in a theorem prover. This article shows ho... Read More about Theorem proving for all: equational reasoning in Liquid Haskell (Functional Pearl).

Parametric polymorphism and operational improvement (2018)
Journal Article

Parametricity, in both operational and denotational forms, has long been a useful tool for reasoning about program correctness. However, there is as yet no comparable technique for reasoning about program improvement, that is, when one program uses f... Read More about Parametric polymorphism and operational improvement.

Compiling a 50-year journey (2017)
Journal Article

Fifty years ago, John McCarthy and James Painter (1967) published the first paper on compiler verification, in which they showed how to formally prove the correctness of a compiler that translates arithmetic expressions into code for a register-based... Read More about Compiling a 50-year journey.

Failing faster: overlapping patterns for property-based testing (2017)
Conference Proceeding

In property-based testing, a key problem is generating input data that satisfies the precondition of a property. One approach is to attempt to do so automatically, from the definition of the precondition itself. This idea has been realised using the... Read More about Failing faster: overlapping patterns for property-based testing.

Contractive Functions on Infinite Data Structures (2016)
Conference Proceeding

Coinductive data structures, such as streams or infinite trees, have many applications in functional programming and type theory, and are naturally defined using recursive equations. But how do we ensure that such equations make sense, i.e. that they... Read More about Contractive Functions on Infinite Data Structures.

Towards a theory of reach (2016)
Journal Article

When testing a program, there are usually some parts that are rarely executed and hence more difficult to test. Finding inputs that guarantee that such parts are executed is an example of a reach problem, which in general seeks to ensure that targete... Read More about Towards a theory of reach.

Cutting out continuations (2016)
Conference Proceeding

In the field of program transformation, one often transforms programs into continuation-passing style to make their flow of control explicit, and then immediately removes the resulting continuations using defunctionalisation to make the programs firs... Read More about Cutting out continuations.

Calculating correct compilers (2015)
Journal Article

© 2016 Cambridge University Press. In this article, we present a new approach to the problem of calculating compilers. In particular, we develop a simple but general technique that allows us to derive correct compilers from high-level semantics by sy... Read More about Calculating correct compilers.

Programs for cheap! (2015)
Conference Proceeding

Write down the definition of a recursion operator on a piece of paper. Tell me its type, but be careful not to let me see the operator’s definition. I will tell you an optimization theorem that the operator satisfies. As an added bonus, I will also g... Read More about Programs for cheap!.

Worker/wrapper/makes it/faster (2014)
Conference Proceeding

Much research in program optimization has focused on formal approaches to correctness: proving that the meaning of programs is preserved by the optimisation. Paradoxically, there has been comparatively little work on formal approaches to efficiency:... Read More about Worker/wrapper/makes it/faster.

Work it, wrap it, fix it, fold it (2014)
Journal Article

The worker/wrapper transformation is a general-purpose technique for refactoring recursive programs to improve their performance. The two previous approaches to formalising the technique were based upon different recursion operators and different cor... Read More about Work it, wrap it, fix it, fold it.

The under-performing unfold: a new approach to optimising corecursive programs (2013)
Conference Proceeding

This paper presents a new approach to optimising corecursive programs by factorisation. In particular, we focus on programs written using the corecursion operator unfold. We use and expand upon the proof techniques of guarded coinduction and unfold f... Read More about The under-performing unfold: a new approach to optimising corecursive programs.