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 21 hours ago

2 days 3 hours ago

2 days 5 hours ago

2 days 15 hours ago

4 days 11 hours ago

5 days 18 hours ago

5 days 18 hours ago

1 week 15 hours ago

1 week 1 day ago

1 week 4 days ago