[TYPES] Types, Processes and Compositional Program Logic.

[Kohei Honda]

Dear colleagues,

I have done a small work on types and process/program logics.
It shows, among others, that types and compositional program
logics are in a tighter relationship than might have been
appreciated before, especially in the context of higher-order
programming languages.

The following link lists several papers related to this
topic. The title and abstract of the main paper are attached
at the end of this mail.

    http://www.dcs.qmul.ac.uk/~kohei/logics

In addition to the main paper, two short papers (2 and 4 in
the web page) would offer concise summaries of some of the
key ideas.

Your comments on this work will be greatly appreciated.

Best wishes,

kohei

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

Title: Process Logic and Duality, Part I.

Author: Kohei Honda (Queen Mary, University of London)

Abstract:

We present typed process logics for the Pi-calculus with
linear/affine type disciplines.  Built on the preceding
studies on logics for programs and processes, simple systems
of assertions are developed, capturing the classes of
behaviours ranging from purely functional processes to those
with destructive update, local state and genericity.
A central feature of the logic is representation of the
environments' behaviour as the dual of those of processes in
assertions, which is crucial for obtaining compositional
proof systems.  This paper develops typed process logics
starting from purely functional behaviours and treating
increasingly complex ones, and illustrate their usage by
deriving program logics for higher-order languages.  The
embedding of the proof rules in the derived logics into the
process logics gives a simple proof of the soundness of the
former.  Some of the derived logics correspond to known
program logics, including Hoare logic for imperative
programs.