The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
Proofs as programs
The work
| Authors | Joseph L. Bates; Robert L. Constable |
|---|---|
| Editors | |
| Type | article |
| Year | 1985 |
| Citekey | bates1985proofs |
Where it appeared
| Published in | ACM Transactions on Programming Languages and Systems |
|---|---|
| Publisher | Association for Computing Machinery (ACM) |
| Volume | 7 |
| Issue | 1 |
| Pages | 113--136 |
Identifiers
| DOI | 10.1145/2363.2528 |
|---|---|
| ISSN | 0164-0925 |
Access
| Landing page | https://doi.org/10.1145/2363.2528 |
|---|
From crossref.
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.
How it got here
| How it got here | agent via crossref |
|---|---|
| Added | 2026-10-25 23:12 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Cite it as
@article{bates1985proofs,
title = {Proofs as programs},
author = {Joseph L. Bates and Robert L. Constable},
year = {1985},
journal = {ACM Transactions on Programming Languages and Systems},
publisher = {Association for Computing Machinery (ACM)},
volume = {7},
number = {1},
pages = {113--136},
issn = {0164-0925},
doi = {10.1145/2363.2528},
}
This record lives at https://refs.drheap.org/bates1985proofs/ and will keep doing so.