Skip Navigation



The Computer Journal Advance Access published online on November 3, 2009
The Computer Journal, doi:10.1093/comjnl/bxp092
This Article
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Honda, K.
Right arrow Articles by Yoshida, N.
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author 2009. Published by Oxford University Press on behalf of The British Computer Society. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

A Unified Theory of Program Logics: An Approach based on the {pi}-Calculus1

Kohei Honda1 and Nobuko Yoshida2,*

1 Department of Computer Science, Queen Mary, University of London, London, UK
2 Department of Computing, Imperial College London, UK

* Corresponding author: yoshida{at}doc.ic.ac.uk

Received 23 September 2009; revised 23 September 2009

Facing staggering diversity of software behaviours in modern and future computing, we argue for the need of a unified theory of program logics, which can capture a general class of software behaviours, as a foundation of software engineering. We propose Hennessy–Milner logic for typed {pi}-calculi as a possible foundation of such a theory. The {pi}-calculus is in 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 semantic theories such as linear logic and game semantics. The embedding of programs in processes leads to the embedding of program logics in the process logic, 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 embedding 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.

Key Words: the {pi}-calculus • types • Hoare logics • Hennessy–Milner logics • relay-guarantee logic • logical full abstraction

Handling editor: Erol Gelenbe

1 A preliminary version of this paper was presented at the BCS08 Visions of Computer Science Conference, held on September 22–24, 2008.


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?




Disclaimer: Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.