A Tool for Verifying Equational Proofs in a Functional Language

Abstract

Equational reasoning is a powerful tool for studying the behavior of functional programs. Learning to write proofs in this style helps a novice programmer to study the behavior of functional programs. However, the verification of these proofs is a tedious process that is prone to human error and lends itself to automation. This paper presents Tigr, a program for verifying the correctness of equational proofs about a simple functional language. Tigr automates the process of proof verification, allowing students to check their work without the need for a human grader. This paper presents the theory behind Tigr, discusses implementation, and demonstrates the use of Tigr to verify actual proofs from an introductory functional programming class.