Home

Ivor, a proof engine

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.

By Niels Hoogeveen at 2006-08-08 13:39 | Functional | Lambda Calculus | Type Theory | other blogs | 6984 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Why invent a new calculus?

First, I find this facinating. I've done a fair bit of work with Coq, but (as a primarily Haskell hacker) I sometimes find the MLisms irritating. I've also occasionally wanted to, eg, automaticlly derive unusual induction principles, but having to work in O'Caml and having to figure out the Coq build system was just too much. A similar Curry-Howard proof/programming system with a more transparent API will be very cool. I'm looking forward to seeing where this work goes! (Integration with Programatica, anyone?)

Second, why invent a new calculus? The paper mentions that TT (the calculus introduced in the paper) is similar to CiC and UTT, etc, but doesn't, as far as I can tell, motivate the need for a new calculus. Why not just adopt one which already has a well studied metatheory? It also seems like using a new calculus limits your interoperability possibilities. Supposing you instead adopted CiC, you could potentially write a translation layer from Coq bytecode and/or XML and get all the results from, eg C-CoRN for free.

By Rob Dockins at Tue, 2006-08-08 15:02 | login or register to post comments