[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Axiom-developer] parametricity

From: Tim Daly
Subject: [Axiom-developer] parametricity
Date: Wed, 7 Nov 2018 14:54:14 -0500

Reynolds is stated as the inventor of parametricity. But it seems to me that the
same idea is stated quite clearly by Dijkstra in 1970 in this note:

In addition, Dijkstra broaches the interesting idea that proofs ought to be constructed
at the level of the flowchart first. Once that is done, using high level steps, it can be
refined into code. But the proof of the code is essentially a refinement of the proof of
the flowchart. This idea is interesting in that it is often the case that a flowchart might
say "find the largest value such that...", which when reduced to code would involve a loop.
A proof that the largest value exists at the abstract "flowchart" level would be easier
to prove than a low-level inductive proof of a program loop that implements the search
and involving issues such as finding invariants.

To my mind, this "hierarchical proof technique" (my words, not Dijkstra's) is rather


reply via email to

[Prev in Thread] Current Thread [Next in Thread]