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.

Two algorithms published as algorithms, each with the paper that proves it correct: Hoare's FIND of 1961 and Quicksort of 1962, both proved in 1971. A course can show the program that was reasoned about beside the reasoning, which is rarer than it sounds.

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