Skip to main content
PRL Project

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.