MobilityReadingGroup

An observationally complete program logic for imperative higher-order functions

Kohei HONDA, Nobuko YOSHIDA, Martin BERGER

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.

@article{HYB2013,
  author = {Kohei Honda and Nobuko Yoshida and Martin Berger},
  title = {{An observationally complete program logic for imperative higher-order functions}},
  journal = {TCS},
  series = {Theoretical Computer Science},
  volume = {517},
  pages = {75--101},
  publisher = {Elsevier},
  year = 2013
}

@article{HYB2013,
  author = {Kohei Honda and Nobuko Yoshida and Martin Berger},
  title = {{An observationally complete program logic for imperative higher-order functions}},
  journal = {Theoretical Computer Science},
  series = {Theoretical Computer Science},
  volume = {517},
  pages = {75--101},
  publisher = {Elsevier},
  doi = "10.1016/j.tcs.2013.11.003",
  year = 2013
}