Soundness of Hoare s Logic: An Automated Proof Using LCF

Stefan Sokolowski. Soundness of Hoare s Logic: An Automated Proof Using LCF. ACM Transactions on Programming Languages and Systems, 9(1):100-120, 1987. [doi]