Dependently Typed Programming based on Automated Theorem Proving

TL;DR

This paper introduces Mella, a minimal dependently typed programming language and theorem prover in Haskell, demonstrating effective integration of automated theorem proving with robust proof reconstruction.

Contribution

It presents a novel integration of Waldmeister into Mella, enabling efficient proof search and reconstruction in dependently typed programming.

Findings

Successfully integrated Waldmeister with Mella on over 800 proof goals

Proof reconstruction in Mella is robust and incurs minimal overhead

Provides a template for integrating advanced theorem provers into dependently typed languages

Abstract

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.