Skip to main content


eCommons@Cornell

eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item: http://hdl.handle.net/1813/6369
Title: Proofs as Programs
Authors: Bates, Joseph L.
Constable, Robert L.
Keywords: computer science
technical report
Issue Date: Feb-1982
Publisher: Cornell University
Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR82-530
Abstract: The significant intellectual cost of programming is for problem solving and explaining and not for coding. Yet, programming systems offer mechanical assistance exclusively with the coding process. Here we describe an implemented program development system, called PRL ("pearl"), that provides automated assistance with the hard part. The program and its explanation are seen as formal objects in a constructive logic of the data domains. These formal explanations can be executed at various stages of completion. The most incomplete explanations resemble applicative programs, the most complete are formal proofs.
URI: http://hdl.handle.net/1813/6369
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
82-530.pdf1.47 MBAdobe PDFView/Open
82-530.ps336.44 kBPostscriptView/Open

Refworks Export

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

 

© 2014 Cornell University Library Contact Us