Visions of Computer Science - BCS International Academic Conference

Imperial College, London, UK - 22 - 24 September 2008

AUTHORS

Kohei Honda & Nobuko Yoshida

ABSTRACT

Facing a staggering diversity of software behaviours in modern and future computing, we argue for the need of a unified theory of program logics for a wide variety of software behaviours as a foundation of software engineering.We propose Hennessy-Milner logic for typed π-calculi as one possible such foundation. The π-calculus enjoys a singular position among computational calculi through its ability to embed sequential and concurrent programs as name passing processes without losing semantic information, and through its connection to other basic theories such as Linear Logic and Game Semantics. The embedding of programs in processes leads to the embedding of logics for programs in the logic for processes, where the observational content of a given program logic is made explicit, analysed and justified on a uniform basis. As a case study, we show embeddings of Hoare logic for sequential programs and a rely-guarantee logic for shared variable concurrency, suggesting that the proposed framework can offer a unifying basis to capture fundamental notions in program logics such as partial/total correctness, sequentiality and different kinds of concurrent computing.

PAPER FORMATS 

PDF Version of this Paper (430kb) 

 

Other Papers in this Session
Other Sessions in this Conference