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

1 day 16 hours ago

2 days 15 hours ago

3 days 9 hours ago

3 days 18 hours ago

5 days 14 hours ago

5 days 20 hours ago

6 days 6 hours ago

6 days 7 hours ago

1 week 2 days ago

1 week 2 days ago