This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.

The program and its proof

A subject the papers are about. The loosest grouping, and the one to reach for last.

Algorithms published as algorithms, each held beside the paper that proves it correct. Collects such pairs so the program reasoned about can be read next to the reasoning. Membership requires the corpus to hold both halves; a proof whose algorithm is absent does not make a pair.

Proof of a Recursive Program: Quicksort

M. Foley and others (1971) · The Computer Journal

Proof of a Program: FIND

C. A. R. Hoare (1971) · Communications of the ACM · Association for Computing Machinery

Quicksort

C. A. R. Hoare (1962) · The Computer Journal

Algorithm 65: find

C. A. R. Hoare (1961) · Communications of the ACM · Association for Computing Machinery

The program and its proof

4 references