Skip navigation
Please use this identifier to cite or link to this item: http://arks.princeton.edu/ark:/88435/dsp01xk81jn70t
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
URI: http://arks.princeton.edu/ark:/88435/dsp01xk81jn70t
Type of Material: Princeton University Senior Theses
Language: en_US
Appears in Collections:Computer Science, 1988-2016

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.