×

Dependently typed programming based on automated theorem proving. (English) Zbl 1358.68056

Gibbons, Jeremy (ed.) et al., Mathematics of program construction. 11th international conference, MPC 2012, Madrid, Spain, June 25–27, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-31112-3/pbk). Lecture Notes in Computer Science 7342, 220-240 (2012).
Summary: 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 this 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.
For the entire collection see [Zbl 1245.68009].

MSC:

68N18 Functional programming and lambda calculus
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI arXiv