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 week 4 days ago
41 weeks 5 days ago
41 weeks 5 days ago
41 weeks 5 days ago
1 year 11 weeks ago
1 year 16 weeks ago
1 year 17 weeks ago
1 year 17 weeks ago
1 year 20 weeks ago
1 year 25 weeks ago