Proofs as programs
- 2 January 1985
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems
- Vol. 7 (1) , 113-136
- https://doi.org/10.1145/2363.2528
Abstract
The significant intellectual cost of programming is for problem solving and explaining, not for coding. Yet programming systems offer mechanical assistance for the coding process exclusively. We illustrate the use of an implemented program development system, called PRL ("pearl"), that provides automated assistance with the difficult part. The problem and its explained solution 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.Keywords
This publication has 13 references indexed in Scilit:
- The Type Theory of PL/CV3ACM Transactions on Programming Languages and Systems, 1984
- Programs as proofs: a synopsisInformation Processing Letters, 1983
- The Cornell program synthesizerCommunications of the ACM, 1981
- A Deductive Approach to Program SynthesisACM Transactions on Programming Languages and Systems, 1980
- A Practical Decision Procedure for Arithmetic with Function SymbolsJournal of the ACM, 1979
- Edinburgh LCFLecture Notes in Computer Science, 1979
- Non-resolution theorem provingArtificial Intelligence, 1977
- Mathematics as a Numerical LanguagePublished by Elsevier ,1970
- An axiomatic basis for computer programmingCommunications of the ACM, 1969
- Semi-Automated MathematicsJournal of the ACM, 1969