Alexander, PerryAustin, Evan Christopher2011-09-222011-09-222011-01-012011http://dissertations.umi.com/ku:11715https://hdl.handle.net/1808/8037HaskHOL is an implementation of a HOL theorem proving capability in Haskell. Motivated by a need to integrate theorem proving capabilities into a Haskell-based tool suite, HaskHOL began as a simple port of HOL Light to Haskell. However, Haskell's laziness, immutable data, and monadic extensions both complicate an implementation and enable a new feature class. This thesis describes HaskHOL, its motivation and implementation. Its use to implement a primitive, interactive theorem prover is explored and its performance is evaluated using a collection of intuitionistically valid problems.82 pagesenThis item is protected by copyright and unless otherwise specified the copyright of this thesis/dissertation is held by the author.Computer scienceHaskellHolTheorem provingThesisopenAccess