Efficiency three ways: tested, verified, and formalised
Two fundamental goals in programming are correctness and efficiency: we want our programs to produce the right results, and to do so using as few resources as possible. One of the key benefits of the functional programming paradigm is the ability to reason about programs as if they are pure mathe...
| Main Author: | |
|---|---|
| Format: | Thesis (University of Nottingham only) |
| Language: | English |
| Published: |
2020
|
| Subjects: | |
| Online Access: | https://eprints.nottingham.ac.uk/63578/ |
| _version_ | 1848800037930270720 |
|---|---|
| author | Handley, Martin AT |
| author_facet | Handley, Martin AT |
| author_sort | Handley, Martin AT |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | Two fundamental goals in programming are correctness and efficiency: we want our programs to produce the right results, and to do so using as few resources as possible.
One of the key benefits of the functional programming paradigm is the ability to reason about programs as if they are pure mathematical functions. In particular, programs can often be proved correct with respect to a specification by exploiting simple algebraic properties akin to secondary school mathematics. On the other hand, program efficiency is not immediately amenable to such algebraic methods used to explore program correctness.
This insight manifests as a reasoning gap between program correctness and efficiency, and is a foundational problem in computer science. Furthermore, it is especially pronounced in lazy functional programming languages such as Haskell, where the on-demand nature of evaluation makes reasoning about efficiency even more challenging.
To aid Haskell programmers in their reasoning about program efficiency, the work in this thesis seeks to partially bridge the reasoning gap using three different approaches: automated testing, semi-formal verification, and formal verification. |
| first_indexed | 2025-11-14T20:45:12Z |
| format | Thesis (University of Nottingham only) |
| id | nottingham-63578 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| language | English |
| last_indexed | 2025-11-14T20:45:12Z |
| publishDate | 2020 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-635782025-02-28T15:05:59Z https://eprints.nottingham.ac.uk/63578/ Efficiency three ways: tested, verified, and formalised Handley, Martin AT Two fundamental goals in programming are correctness and efficiency: we want our programs to produce the right results, and to do so using as few resources as possible. One of the key benefits of the functional programming paradigm is the ability to reason about programs as if they are pure mathematical functions. In particular, programs can often be proved correct with respect to a specification by exploiting simple algebraic properties akin to secondary school mathematics. On the other hand, program efficiency is not immediately amenable to such algebraic methods used to explore program correctness. This insight manifests as a reasoning gap between program correctness and efficiency, and is a foundational problem in computer science. Furthermore, it is especially pronounced in lazy functional programming languages such as Haskell, where the on-demand nature of evaluation makes reasoning about efficiency even more challenging. To aid Haskell programmers in their reasoning about program efficiency, the work in this thesis seeks to partially bridge the reasoning gap using three different approaches: automated testing, semi-formal verification, and formal verification. 2020-12-11 Thesis (University of Nottingham only) NonPeerReviewed application/pdf en arr https://eprints.nottingham.ac.uk/63578/1/thesis.pdf Handley, Martin AT (2020) Efficiency three ways: tested, verified, and formalised. PhD thesis, University of Nottingham. Efficiency Correctness Program verification Program analysis Formal reasoning Static analysis Functional programming. |
| spellingShingle | Efficiency Correctness Program verification Program analysis Formal reasoning Static analysis Functional programming. Handley, Martin AT Efficiency three ways: tested, verified, and formalised |
| title | Efficiency three ways: tested, verified, and formalised |
| title_full | Efficiency three ways: tested, verified, and formalised |
| title_fullStr | Efficiency three ways: tested, verified, and formalised |
| title_full_unstemmed | Efficiency three ways: tested, verified, and formalised |
| title_short | Efficiency three ways: tested, verified, and formalised |
| title_sort | efficiency three ways: tested, verified, and formalised |
| topic | Efficiency Correctness Program verification Program analysis Formal reasoning Static analysis Functional programming. |
| url | https://eprints.nottingham.ac.uk/63578/ |