I found an interesting new paper by Edwin Brady.

Abstract. Dependent type theory has several practical applications in

the fields of theorem proving, program verifcation and programming

language design. Ivor is a Haskell library designed to allow easy extend-

ing 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 implement formal systems such as propositional

logic. Furthermore, I sketch an implementation of a simple functional

programming language using the library; by using type theory as a core

representation, we can construct and evaluate terms and prove correct-

ness properties of those terms within the same framework, ensuring con-

sistency of the implementation and the theorem prover.

## Recent comments

20 hours 30 min ago

3 days 4 hours ago

3 days 7 hours ago

4 days 2 hours ago

4 days 9 hours ago

4 days 13 hours ago

4 days 13 hours ago

4 days 16 hours ago

5 days 7 hours ago

5 days 11 hours ago