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.