[PRL] Dependently Typed Programming based on Automated Theorem Proving | Lambda the Ultimate

[Mitchell Wand]

Unread, fwiw.


> 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.


http://lambda-the-ultimate.org/node/4423
-------------- next part --------------
HTML attachment scrubbed and removed