Program Logics

A Compositional Program Logic for Imperative Higher-Order Functions (full version)  
Kohei Honda, Nobuko Yoshida and Martin Berger (October, 2004; Updated November, 2004).
[ps-file]

The extended abstract of the above paper.
[ps-file] (October, 2004).

Reference


From Process Logic to Program Logic
Kohei Honda.
9th ACM-SIGPLAN International Conference on Functional Programming (ICFP 04), ACM Press, 2004.
[ps-file]

A Compositional Program Logic for Polymorphic Higher-Order Functions
Kohei Honda and Nobuko Yoshida.
6th ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP'2004), ACM Press, 2004.
[ps-file]

More references available from http://www.dcs.qmul.ac.uk/~kohei/logics/index.html