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
Archive Status
This item contains archived web content.
Files
Research Projects
Organizational Units
Journal Issue
Keywords
Computer science, Haskell, Hol, Theorem proving