Efficiency three ways: tested, verified, and formalised
Publication Date
December 11, 2020
Creator
Abstract
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.
Item Type
ethesis
Thesis Type
PhD
Supervisors
Subjects (LC)
Associated Schools / Departments
School of Computer Science (UK)
eprints ID
63578
UoN Repository URI
Except where otherwise noted, this item's license is described as
File(s)![Thumbnail Image]()
Name
thesis.pdf
Type
Full-text
Description
Examined
Size
3.45 MB
Format
Adobe PDF
Checksum (MD5)
223219c6b08f68e029c18f941fd2dcf1