From process logic to program logic

We present a process logic for the -calculus with the linear/affine type discipline (Berger et al. 2001; Berger et al. 2003; Honda and Yoshida 2002; Honda and Yoshida 2003; Honda et al. 2004; Yoshida et al. 2001; Yoshida et al. 2002). 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 interactions to those with destructive update, local state and genericity. A central feature of the logic is representation of the behaviour of an environment as the dual of that of a process in an assertion, which is crucial for obtaining compositional proof systems. From the process logic we can derive compositional program logics for various higher-order programming languages, whose soundness is proved via their embeddings into the process logic. In this paper, the key technical framework of the process logic and its applications is presented focussing on pure functional beh...

• Type: Conference
• Year: 2004
• Where: ICFP
• Authors: Kohei Honda
• Keywords: Honda Et, ICFP 2004, Process Logic, Programming Languages, Yoshida Et