Logical Reasoning for Higher-Order Functions with Local State

Reference

Descriptive and Relative Completeness for Higher-Order Functions (full version)
Kohei Honda, Martin Berger and Nobuko Yoshida (July, 2006).
[pdf-file]
which prove completeness properties of logics for higher-order functions. (the extended abstract presented at ICALP'06, Venice, July 2006)

A Logical Analysis of Aliasing in Imperative Higher-Order Functions (extended abstract)
Martin Berger, Kohei Honda and Nobuko Yoshida,
ICFP'05, 10th ACM-SIGPLAN International Conference on Functional Programming (ICFP 05), ACM Press, 2005.
[pdf-file]

A Logical Analysis of Aliasing in Imperative Higher-Order Functions (full version)
Martin Berger, Kohei Honda and Nobuko Yoshida (July, 2007).
[pdf-file]
A simple logical articulation of the general forms of aliasing for imperative higher-order functions.

An Observationally Complete Program Logic for Imperative Higher-Order Functions (full version)
Kohei Honda, Nobuko Yoshida and Martin Berger (January 2005).
[pdf-file]
The full account of a basic logic for sequential higher-order functions with global state with a precise tie with observational semantics.
Section 8 includes extensive historical survey.

An Observationally Complete Program Logic for Imperative Higher-Order Functions (extended abstract) 20th Annual IEEE Symposium on Logic in Computer Science (LICS 2005), 270--279.
[pdf-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.
[pdf-file]
A program logic for polymorphic higher-order functions.

From Process Logic to Program Logic
Kohei Honda.
9th ACM-SIGPLAN International Conference on Functional Programming (ICFP 04), ACM Press, 2004.
[pdf-file]
A brief introduction to the key technical ideas in the purely functional setting.

More references available from www.doc.ic.ac.uk/~yoshida