Agda is a dependently typed functional programming language and a proof assistant in which developing programs and proving their correctness is one activity. We show how this process can be enhanced by integrating external automated theorem provers, provide a prototypical integration of the equational theorem prover Waldmeister, and give examples of how this proof automation works in practice. © 2011 Springer-Verlag.
CITATION STYLE
Foster, S., & Struth, G. (2011). Integrating an automated theorem prover into Agda. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6617 LNCS, pp. 116–130). https://doi.org/10.1007/978-3-642-20398-5_10
Mendeley helps you to discover research relevant for your work.