A Constructive Programming Logic
by Robert L. Constable
In Information Processing 77, B. Gilchrist, Editor
IFIP, North-Holland Publishing Company (1977)
Proceedings of IFIP Congress 77
Toronto, August 8-12, 1977
We describe a constructive logic for reasoning about and developing Algol-like programs. We discuss its role in programming and program verification, emphasizing the consequences of its underlying computational semantics. We briefly consider an implemented verification system, PL/CV, based on this logic.