Loading...
HaskHOL: A Haskell Hosted Domain Specific Language for Higher-Order Logic Theorem Proving
Austin, Evan Christopher
Austin, Evan Christopher
Citations
Altmetric:
Abstract
HaskHOL 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.
Description
Date
2011-01-01
Journal Title
Journal ISSN
Volume Title
Publisher
University of Kansas
Collections
Research Projects
Organizational Units
Journal Issue
Keywords
Computer science, Haskell, Hol, Theorem proving