Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Twentieth Annual IEEE Symposium on

Logic in Computer Science (LICS 2005)

Paper: An Observationally Complete Program Logic for Imperative Higher-Order Frame Rules (at LICS 2005)

Authors: Kohei Honda Nobuko Yoshida Martin Berger

Abstract

We propose a simple compositional program logic for an imperative extension of call-by-value PCF, built on Hoare logic and our preceding work on program logics for pure higher-order functions. A systematic use of names and operations on them allows precise and general description of complex higher-order imperative behaviour. The logic offers a foundation for general treatment of aliasing and local state on its basis, with minimal extensions. After establishing soundness, we prove that valid assertions for programs completely characterise their behaviour up to observational congruence, which is proved using a variant of finite canonical forms. The use of the logic is illustrated through reasoning examples which are hard to assert and infer using existing program logics.

BibTeX

  @InProceedings{HondaYoshidaBerger-AnObservationallyCo,
    author = 	 {Kohei Honda and Nobuko Yoshida and Martin Berger},
    title = 	 {An Observationally Complete Program Logic for Imperative Higher-Order Frame Rules},
    booktitle =  {Proceedings of the Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS 2005)},
    year =	 {2005},
    month =	 {June}, 
    pages =      {270--279},
    location =   {Chicago, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski