All Outputs (55)

Calculating Compilers Effectively (Functional Pearl) (2024)
Presentation / Conference Contribution
Garby, Z., Hutton, G., & Bahr, P. (2024, September). Calculating Compilers Effectively (Functional Pearl). Presented at Haskell '24: 17th ACM SIGPLAN International Haskell Symposium, Milan, Italy

Much work in the area of compiler calculation has focused on pure languages. While this simplifies the reasoning, it reduces the applicability. In this article, we show how an existing compiler calculation methodology can be naturally extended to lan... Read More about Calculating Compilers Effectively (Functional Pearl).

Beyond Trees: Calculating Graph-Based Compilers (Functional Pearl) (2024)
Journal Article
Bahr, P., & Hutton, G. (2024). Beyond Trees: Calculating Graph-Based Compilers (Functional Pearl). Proceedings of the ACM on Programming Languages, 8(ICFP), 370-394. https://doi.org/10.1145/3674638

Bahr and Hutton recently developed an approach to compiler calculation that allows a wide range of compilers to be derived from specifications of their correctness. However, a limitation of the approach is that it results in compilers that produce tr... Read More about Beyond Trees: Calculating Graph-Based Compilers (Functional Pearl).

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.

Programming language semantics: It’s easy as 1,2,3 (2023)
Journal Article
HUTTON, G. (2023). Programming language semantics: It’s easy as 1,2,3. Journal of Functional Programming, 33, Article e9. https://doi.org/10.1017/S0956796823000072

Programming language semantics is an important topic in theoretical computer science, but one that beginners often find challenging. This article provides a tutorial introduction to the subject, in which the language of integers and addition is used... Read More about Programming language semantics: It’s easy as 1,2,3.

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.

Subtyping Without Reduction (2022)
Presentation / Conference Contribution
Hewer, B., & Hutton, G. (2022, September). Subtyping Without Reduction. Presented at 14th International Conference, MPC 2022, Tbilisi, Georgia

Subtypes are useful and ubiquitous, allowing important properties of data to be captured directly in types. However, the standard encoding of subtypes gives no control over when the reduction of subtyping proofs takes place, which can significantly i... Read More about Subtyping Without Reduction.

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, Article e25. 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.

Liquidate your assets: reasoning about resource usage in liquid Haskell (2019)
Presentation / Conference Contribution
Handley, M., Vazou, N., & Hutton, G. Liquidate your assets: reasoning about resource usage in liquid Haskell. Presented at 47th ACM SIGPLAN Symposium on Principles of Programming Languages, New Orleans, Louisiana, USA

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
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)
Presentation / Conference Contribution
HANDLEY, M., & HUTTON, G. (2018, September). AutoBench: comparing the time performance of Haskell programs. Presented at 11th ACM SIGPLAN International Symposium on Haskell

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)
Presentation / Conference Contribution
Vazou, N., Breitner, J., Kunkel, R., Van Horn, D., & Hutton, G. (2018, September). Theorem proving for all: equational reasoning in liquid Haskell (functional pearl). Presented at ICFP '18: 23nd ACM SIGPLAN International Conference on Functional Programming, St. Louis MO USA

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)
Presentation / Conference Contribution
Hackett, J., & Hutton, G. Parametric polymorphism and operational improvement. Presented at 23rd ACM SIGPLAN International Conference on Functional Programming, St. Louis, Missouri, United States

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. https://doi.org/10.1017/S0956796817000120

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)
Presentation / Conference Contribution
Fowler, J., & Hutton, G. (2017, January). Failing faster: overlapping patterns for property-based testing. Presented at 19th International Symposium on Practical Aspects of Declarative Languages

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)
Presentation / Conference Contribution
Capretta, V., Hutton, G., & Jaskelioff, M. (2016, August). Contractive Functions on Infinite Data Structures. Presented at 28th Symposium on Implementation and Application of Functional Languages, Leuven, Belgium

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
Fowler, J., & Hutton, G. (2016). Towards a theory of reach. Lecture Notes in Artificial Intelligence, 9547, https://doi.org/10.1007/978-3-319-39110-6

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)
Presentation / Conference Contribution
Hutton, G., & Bahr, P. Cutting out continuations. Presented at WadlerFest

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.