Please use this identifier to cite or link to this item:
|Title:||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.|
|Type of Material:||Princeton University Senior Theses|
|Appears in Collections:||Computer Science, 1988-2017|
Files in This Item:
|PUTheses2015-Grasso_Andrew.pdf||308.16 kB||Adobe PDF||Request a copy|
Items in Dataspace are protected by copyright, with all rights reserved, unless otherwise indicated.