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
4 days 7 hours ago
6 days 1 hour ago
2 weeks 3 days ago
3 weeks 2 days ago
4 weeks 2 days ago
6 weeks 7 hours ago
6 weeks 3 days ago
7 weeks 4 days ago
8 weeks 10 hours ago
8 weeks 14 hours ago