Skip to main content

Research Repository

Advanced Search

All Outputs (49)

Quotient Haskell: Lightweight Quotient Types for All (2024)
Journal Article
Hewer, B., & Hutton, G. (2024). Quotient Haskell: Lightweight Quotient Types for All. Proceedings of the ACM on Programming Languages, 8(POPL), 785-815. https://doi.org/10.1145/3632869

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
Bahr, P., & Hutton, G. (2023). Calculating Compilers for Concurrency. Proceedings of the ACM on Programming Languages, 7(ICFP), 740-767. https://doi.org/10.1145/3607855

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, P., & Hutton, G. (2022). Monadic compiler calculation (functional pearl). Proceedings of the ACM on Programming Languages, 6(ICFP), 80-108. https://doi.org/10.1145/3547624

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
Pickard, M., & Hutton, G. (2021). Calculating dependently-typed compilers (functional pearl). Proceedings of the ACM on Programming Languages, 5(ICFP), 1-27. https://doi.org/10.1145/3473587

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
Bahr, P., & Hutton, G. (2020). Calculating correct compilers II: Return of the register machines. Journal of Functional Programming, 30, https://doi.org/10.1017/s0956796820000209

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.

Call-by-need is clairvoyant call-by-value (2019)
Journal Article
Hackett, J., & Hutton, G. (2019). Call-by-need is clairvoyant call-by-value. Proceedings of the ACM on Programming Languages, 3(ICFP), 1-21. https://doi.org/10.1145/3341718

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
HANDLEY, M., & HUTTON, G. (2018). AutoBench: comparing the time performance of Haskell programs. In Proceedings of the 11th ACM SIGPLAN Haskell Symposium (Haskell '18). , (26-37). https://doi.org/10.1145/3242744.3242749

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
Vazou, N., Breitner, J., Kunkel, R., Van Horn, D., & Hutton, G. (2018). Theorem proving for all: equational reasoning in Liquid Haskell (Functional Pearl). In Proceedings of the 11th ACM SIGPLAN Haskell Symposium (Haskell '18) (132-144). https://doi.org/10.1145/3242744.3242756

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
Hackett, J., & Hutton, G. (2018). Parametric polymorphism and operational improvement. Proceedings of the ACM on Programming Languages, 2(ICFP), 1-24. https://doi.org/10.1145/3236763

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
Hutton, G., & Bahr, P. (2017). Compiling a 50-year journey. Journal of Functional Programming, 27, Article e20

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
Fowler, J., & Hutton, G. (2017). Failing faster: overlapping patterns for property-based testing. In Practical Aspects of Declarative Languages: 19th International Symposium, PADL 2017, Paris, France, January 16-17, 2017: Proceedings (103-119). https://doi.org/10.1007/978-3-319-51676-9-7

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
Capretta, V., Hutton, G., & Jaskelioff, M. (2016). Contractive Functions on Infinite Data Structures. In IFL 2016: Proceedings of the 28th Symposium on the Implementation and Application of Functional Programming Languages (1-13). https://doi.org/10.1145/3064899.3064900

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.

Cutting out continuations (2016)
Conference Proceeding
Hutton, G., & Bahr, P. (2016). Cutting out continuations.

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
Bahr, P., & Hutton, G. (2015). Calculating correct compilers. Journal of Functional Programming, 25, Article e14. https://doi.org/10.1017/S0956796815000180

© 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
Hackett, J., & Hutton, G. (2015). Programs for cheap!. In Proceedings of the 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (115-126). https://doi.org/10.1109/LICS.2015.21

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
Hackett, J., & Hutton, G. (2014). Worker/wrapper/makes it/faster.

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
Sculthorpe, N., & Hutton, G. (2014). Work it, wrap it, fix it, fold it. Journal of Functional Programming, 24(1), https://doi.org/10.1017/S0956796814000045

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
Hackett, J., Hutton, G., & Jaskelioff, M. (2013). The under-performing unfold: a new approach to optimising corecursive programs.

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.