A Hoare Calculus for functions defined by recursion on higher types

Goerdt, A. (1985). A Hoare Calculus for functions defined by recursion on higher types. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 193 LNCS, pp. 106–117). Springer Verlag. https://doi.org/10.1007/3-540-15648-8_9