All Outputs (21)

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.

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.

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.

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.

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.

Report on BCTCS 2005 (2005)
Journal Article

This report contains edited abstracts from BCTCS 2005, which was held on 22nd to 24th March 2005 in Nottingham, England.

Proof Methods for Corecursive Programs (2005)
Journal Article

Recursion is a well-known and powerful programming technique, with a wide variety of applications. The dual technique of corecursion is less well-known, but is increasingly proving to be just as useful. This article is a tutorial on the four main m... Read More about Proof Methods for Corecursive Programs.

The Countdown Problem (2002)
Journal Article

We systematically develop a functional program that solves the countdown problem, a numbers game in which the aim is to construct arithmetic expressions satisfying certain constraints. Starting from a formal specification of the problem, we present... Read More about The Countdown Problem.

The Generic Approximation Lemma (2001)
Journal Article

The approximation lemma is a simplification of the well-known take lemma, and is used to prove properties of programs that produce lists of values. We show how the approximation lemma, unlike the take lemma, can naturally be generalised from lists t... Read More about The Generic Approximation Lemma.

A Tutorial on the Universality and Expressiveness of Fold (1999)
Journal Article

In functional programming, fold is a standard operator that encapsulates a simple pattern of recursion for processing lists. This article is a tutorial on two key aspects of the fold operator for lists. First of all, we emphasize the use of the uni... Read More about A Tutorial on the Universality and Expressiveness of Fold.

Monadic parsing in Haskell (1998)
Journal Article

This paper is a tutorial on defining recursive descent parsers in Haskell. In the spirit of one-stop shopping, the paper combines material from three areas into a single source. The three areas are functional parsers, the use of monads to structure... Read More about Monadic parsing in Haskell.

Back to Basics: Deriving Representation Changers Functionally (1996)
Journal Article

Many functional programs can be viewed as representation changers, that is, as functions that convert abstract values from one concrete representation to another. Examples of such programs include base-converters, binary adders and multipliers, and... Read More about Back to Basics: Deriving Representation Changers Functionally.

Review of Mike Gordon and Tom Melham (editors), An Introduction to HOL, a Theorem Proving Environment for Higher Order Logic (1994)
Journal Article