Ivor, a Proof Engine

摘要

Dependent type theory has several practical applications in the fields of theorem proving, program verification and programming language design. Ivor is a Haskell library designed to allow easy extending and embedding of a type theory based theorem prover in a Haskell application. In this paper, I give an overview of the library and show how it can be used to embed theorem proving technology in an implementation of a simple functional programming language; by using type theory as a core representation, we can construct and evaluate terms and prove correctness properties of those terms within the same framework, ensuring consistency of the implementation and the theorem prover.