eCommons

 

Proofs as Programs

dc.contributor.authorBates, Joseph L.en_US
dc.contributor.authorConstable, Robert L.en_US
dc.date.accessioned2007-04-23T16:46:15Z
dc.date.available2007-04-23T16:46:15Z
dc.date.issued1982-02en_US
dc.description.abstractThe 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.en_US
dc.format.extent1504756 bytes
dc.format.extent344513 bytes
dc.format.mimetypeapplication/pdf
dc.format.mimetypeapplication/postscript
dc.identifier.citationhttp://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR82-530en_US
dc.identifier.urihttps://hdl.handle.net/1813/6369
dc.language.isoen_USen_US
dc.publisherCornell Universityen_US
dc.subjectcomputer scienceen_US
dc.subjecttechnical reporten_US
dc.titleProofs as Programsen_US
dc.typetechnical reporten_US

Files

Original bundle
Now showing 1 - 2 of 2
Loading...
Thumbnail Image
Name:
82-530.pdf
Size:
1.44 MB
Format:
Adobe Portable Document Format
No Thumbnail Available
Name:
82-530.ps
Size:
336.44 KB
Format:
Postscript Files