An observationally complete program logic for imperative higher-order functions

Honda, Kohei, Yoshida, Nobuko and Berger, Martin (2014) An observationally complete program logic for imperative higher-order functions. Theoretical Computer Science, 517. pp. 75-101. ISSN 0304-3975

[img] PDF - Published Version
Download (508kB)


We establish a strong completeness property called observational completeness of the program logic for imperative, higher-order functions introduced in [1]. Observational completeness states that valid assertions characterise program behaviour up to observational congruence, giving a precise correspondence between operational and axiomatic semantics. The proof layout for the observational completeness which uses a restricted syntactic structure called finite canonical forms originally introduced in game-based semantics, and characteristic formulae originally introduced in the process calculi, is generally applicable for a precise axiomatic characterisation of more complex program behaviour, such as aliasing and local state.

Item Type: Article
Keywords: CompletenessCharacteristic formulaeProgram logicHigher-order functionImperative programmingObservational equivalence
Schools and Departments: School of Engineering and Informatics > Informatics
Research Centres and Groups: Foundations of Software Systems
Depositing User: Martin Berger
Date Deposited: 18 Dec 2017 15:44
Last Modified: 02 Jul 2019 17:04

View download statistics for this item

📧 Request an update