Title: An LCF proof of soundness of Hoare's logic
First published: 1983