[TYPES] Program logics for imperative higher-order functions and aliasing.

[Kohei Honda]

Dear colleagues,

I would like to announce two works on program logics for imperative
higher-order functions and aliasing. A close tie between types,
observational semantics and program logics is an underpinning of
these works.

Your comments on these works are warmly welcome.

Best wishes,

Kohei Honda     (kohei at dcs.qmul.ac.uk)
Martin Berger   (martinb at dcs.qmul.ac.uk)
Nobuko Yoshida  (yoshida at doc.ic.ac.uk)

(imperative higher-order functions)
http://www.dcs.qmul.ac.uk/~kohei/logics/imperative1short.ps  (short)
http://www.dcs.qmul.ac.uk/~kohei/logics/imperative1.ps       (long)

(aliasing)
http://www.dcs.qmul.ac.uk/~kohei/logics/imperative2short.ps  (short)
http://www.dcs.qmul.ac.uk/~kohei/logics/imperative2.ps       (long)

--------------------------------------------------------------------

Title: Observationally Complete Program Logic for Imperative
        Higher-Order Functions.

Abstract:
We propose a simple compositional program logic for an imperative
extension of call-by-value PCF, built on Hoare logic and our
preceding work on program logics for pure higher-order functions.
A systematic use of names and operations on them allows precise
and general description of complex higher-order imperative behaviour.
The logic offers a foundation for general treatment of aliasing
and local state on its basis, with minimal extensions. After
establishing soundness, we prove that valid assertions for programs
completely characterise their behaviour up to observational
congruence, which is proved using a variant of finite canonical
forms. The use of the logic is illustrated through reasoning
examples which are hard to assert and infer using existing program
logics.

(to appear in LICS'05)

---------------------------------------------------------------------

Title: A Logical Analysis of Aliasing in Imperative Higher-Order
        Functions.

Abstract:
We present a compositional program logic for call-by-value imperative
higher-order functions with general forms of aliasing, which can arise
from the use of reference names as function parameters, return values,
content of references and parts of data structures.  The program logic
extends our earlier logic for alias-free imperative higher-order
functions with new modal operators which serve as building blocks for
clean structural reasoning about programs and data structures in the
presence of aliasing, which has been an open issue since the
pioneering work by Cartwright-Oppen and Morris twenty-five years
ago. We illustrate usage of the logic for description and reasoning
through concrete examples including a higher-order polymorphic
Quicksort.  The logical status of the new operators is clarified by
translating them into (in)equalities of reference names. The logic is
observationally complete in the sense that two programs are
observationally indistinguishable iff they satisfy the same set of
assertions.