JavaScript is disabled for your browser. Some features of this site may not work without it.
Proofs as Programs

Author
Bates, Joseph L.; Constable, Robert L.
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.
Date Issued
1982-02Publisher
Cornell University
Subject
computer science; technical report
Previously Published As
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR82-530
Type
technical report