Outputs (53)

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).

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.

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.

Programs for cheap! (2015)
Presentation / Conference Contribution
Hackett, J., & Hutton, G. (2015, July). Programs for cheap!. Presented at Thirtieth Annual ACM/IEEE Symposium on Logic in Computer Science, Kyoto, Japan

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!.