Dependently Typed Programming based on Automated Theorem Proving

Dependently Typed Programming based on Automated Theorem Proving, by Alasdair Armstrong, Simon Foster, and Georg Struth. [Link to preprint on ArXiv, a.k.a. this has not yet been refereed, use at your own risk].

Mella is a minimalistic dependently typed programming language and interactive theorem prover implemented in Haskell. Its main purpose is to investigate the effective integration of automated theorem provers in a pure and simple setting. Such integrations are essential for supporting program development in dependently typed languages. We integrate the equational theorem prover Waldmeister and test it on more than 800 proof goals from the TPTP library. In contrast to previous approaches, the reconstruction of Waldmeister proofs within Mella is quite robust and does not generate a significant overhead to proof search. Mella thus yields a template for integrating more expressive theorem provers in more sophisticated languages.

Coq and Agda are demonstrating the dependently-typed programming is feasible and beneficial -- but still quite painful in practice. The point of computers is that they can automate a lot of drudgery. And a lot of proofs ought to be considered drudgery as well. But, in practice, this is a huge leap. The authors present an interesting experiment in a promising direction.

The LtU angle here is that current (automated) proof assistants generate proofs which, usually, have a huge impedance mismatch with the kinds of evidence that a type-checker for a dependently-typed language needs to be convinced of the validity of some user code. So there is a non-trivial engineering issue to be solved regarding the implementation of a pleasant environment for dependently-typed programming.

Comment viewing options

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

What is elimJ?

Dear All,

Was just wondering what the elimJ axiom is, and found the following interesting blog entry:


Not sure whether the resulting logic matches the logic of Waldmeister? Maybe a mismatch would explain the reconstruction failures?

How about ATS?

I am actually new in dependent types, but I have some experience with Coq, and now I'm studying ATS.
It provides ways of changing state (i.e. has variables), of memory allocating and other imperative features, using proofs such as "memory is allocated", "now variable has value 'x'".
And in addition it translates to plain C and is compiled by gcc.
I think it should be taken into consideration.
It's new way of understanding of imperative programming.

p.s. to be honest It has very abnormal syntax.

Can I get it?

Is it possible to have a copy of Mella?

Thanks a lot!

edit: sorry, I hurried, and now I have got it.