ATTENTION: The software behind KU ScholarWorks is being upgraded to a new version. Starting July 15th, users will not be able to log in to the system, add items, nor make any changes until the new version is in place at the end of July. Searching for articles and opening files will continue to work while the system is being updated.
If you have any questions, please contact Marianne Reed at mreed@ku.edu .
HERMIT: Mechanized Reasoning during Compilation in the Glasgow Haskell Compiler
dc.contributor.advisor | Gill, Andrew | |
dc.contributor.author | Farmer, Andrew | |
dc.date.accessioned | 2016-01-01T22:20:58Z | |
dc.date.available | 2016-01-01T22:20:58Z | |
dc.date.issued | 2015-05-31 | |
dc.date.submitted | 2015 | |
dc.identifier.other | http://dissertations.umi.com/ku:14110 | |
dc.identifier.uri | http://hdl.handle.net/1808/19416 | |
dc.description.abstract | It is difficult to write programs which are both correct and fast. A promising approach, functional programming, is based on the idea of using pure, mathematical functions to construct programs. With effort, it is possible to establish a connection between a specification written in a functional language, which has been proven correct, and a fast implementation, via program transformation. When practiced in the functional programming community, this style of reasoning is still typically performed by hand, by either modifying the source code or using pen-and-paper. Unfortunately, performing such semi-formal reasoning by directly modifying the source code often obfuscates the program, and pen-and-paper reasoning becomes outdated as the program changes over time. Even so, this semi-formal reasoning prevails because formal reasoning is time-consuming, and requires considerable expertise. Formal reasoning tools often only work for a subset of the target language, or require programs to be implemented in a custom language for reasoning. This dissertation investigates a solution, called HERMIT, which mechanizes reasoning during compilation. HERMIT can be used to prove properties about programs written in the Haskell functional programming language, or transform them to improve their performance. Reasoning in HERMIT proceeds in a style familiar to practitioners of pen-and-paper reasoning, and mechanization allows these techniques to be applied to real-world programs with greater confidence. HERMIT can also re-check recorded reasoning steps on subsequent compilations, enforcing a connection with the program as the program is developed. HERMIT is the first system capable of directly reasoning about the full Haskell language. The design and implementation of HERMIT, motivated both by typical reasoning tasks and HERMIT's place in the Haskell ecosystem, is presented in detail. Three case studies investigate HERMIT's capability to reason in practice. These case studies demonstrate that semi-formal reasoning with HERMIT lowers the barrier to writing programs which are both correct and fast. | |
dc.format.extent | 213 pages | |
dc.language.iso | en | |
dc.publisher | University of Kansas | |
dc.rights | Copyright held by the author. | |
dc.subject | Computer science | |
dc.subject | Equational Reasoning | |
dc.subject | GHC | |
dc.subject | Haskell | |
dc.subject | Program Transformation | |
dc.title | HERMIT: Mechanized Reasoning during Compilation in the Glasgow Haskell Compiler | |
dc.type | Dissertation | |
dc.contributor.cmtemember | Alexander, Perry | |
dc.contributor.cmtemember | Kulkarni, Prasad | |
dc.contributor.cmtemember | Miller, James | |
dc.contributor.cmtemember | Depcik, Christopher | |
dc.thesis.degreeDiscipline | Electrical Engineering & Computer Science | |
dc.thesis.degreeLevel | Ph.D. | |
dc.rights.accessrights | openAccess |
Files in this item
This item appears in the following Collection(s)
-
Dissertations [4889]
-
Engineering Dissertations and Theses [1055]