Proving Properties of Programs by Structural Induction
The work
| Authors | Rod M. Burstall |
|---|---|
| Editors | |
| Type | article |
| Year | 1969 |
| Citekey | burstall1969proving |
Where it appeared
| Published in | The Computer Journal |
|---|---|
| Publisher | Oxford University Press |
| Volume | 12 |
| Issue | 1 |
| Pages | 41--48 |
Identifiers
| DOI | 10.1093/comjnl/12.1.41 |
|---|---|
| OpenAlex | W2159709550 |
Access
| Landing page | https://doi.org/10.1093/comjnl/12.1.41 |
|---|
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
Abstract
This paper discusses the technique of structural induction for proving theorems about programs. This technique is closely related to recursion induction but makes use of the inductive definition of the data structures handled by the programs. It treats programs with recursion but without assignments or jumps. Some syntactic extensions to Landin's functional programming language ISWIM are suggested which make it easier to program the manipulation of data structures and to develop proofs about such programs. Two sample proofs are given to demonstrate the technique, one for a tree sorting algorithm and one for a simple compiler for expressions.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-25 05:14 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Cite it as
@article{burstall1969proving,
title = {Proving Properties of Programs by Structural Induction},
author = {Rod M. Burstall},
year = {1969},
journal = {The Computer Journal},
publisher = {Oxford University Press},
volume = {12},
number = {1},
pages = {41--48},
doi = {10.1093/comjnl/12.1.41},
}
This record lives at https://refs.drheap.org/burstall1969proving/ and will keep doing so.