Skip navigation
Please use this identifier to cite or link to this item:
Title: A Tool for Verifying Equational Proofs in a Functional Language
Authors: Grasso, Andrew
Advisors: Walker, David
Department: Computer Science
Class Year: 2015
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.
Extent: 45 pages
Type of Material: Princeton University Senior Theses
Language: en_US
Appears in Collections:Computer Science, 1988-2017

Files in This Item:
File SizeFormat 
PUTheses2015-Grasso_Andrew.pdf308.16 kBAdobe PDF    Request a copy

Items in Dataspace are protected by copyright, with all rights reserved, unless otherwise indicated.