Personal tools
You are here: Home Events Abstract Archives 2004 From Process Logics to Program Logics

From Process Logics to Program Logics

Kohei Honda Department of Computer Science Queen Mary, University of London 2pm 25 June 2004 Room 2511, JCMB, King's Buildings

This talk discusses how one can derive a compositional program logic for higher-order programming languages from a compositional logic for typed pi-calculi.

Built on the preceding studies on logics for programs and processes, simple systems of assertions are developed, capturing the classes of behaviours ranging from pure higher-order functions to those with destructive update, local state and polymorphism.

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 talk concentrates on pure functional processes, discussing how a process logic for them leads to a program logic for call-by-value PCF via fully abstract encoding. The embedding of the derived logic in the process logic gives a simple proof of the soundness of the former via logical full abstraction in the sense of Longley and Plotkin.

If time allows, we shall also mention stateful extensions of this logic, some of which correspond to known program logics, including Hoare logic for imperative programs.

Document Actions