[moca] Logics for Processes, Logics for Programs.

[kohei@xxxxxxxxxxxxxx]

Dear colleagues,

I have done a small work on logics for the pi-calculus.

Its aim is to have a compositional logic for typed processes,
and use it to derive, verify and mediate compositional
program logics for individual programming languages. As a
whole, it aims to offer a language-independent framework for
compositional reasoning of general software behaviour.

Such a framework is necessary when, for example, we wish to
reason about behaviour of multi-lingual software (in fact
if we run a Java program under an OS written in C/C++, this
is already multi-lingual).

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 technical ideas.

Your comments on this work are warmly welcome.

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.





  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
 http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html