811
views
0
recommends
+1 Recommend
1 collections
    4
    shares

      Celebrating 65 years of The Computer Journal - free-to-read perspectives - bcs.org/tcj65

      scite_
       
      • Record: found
      • Abstract: found
      • Conference Proceedings: found
      Is Open Access

      A Unified Theory of Program Logics: An Approach based on the π-Calculus

      proceedings-article
      ,
      Visions of Computer Science - BCS International Academic Conference (VOCS)
      BCS International Academic Conference
      22 - 24 September 2008
      The π-calculus, Types, Hoare logics, Hennessy-Milner logics, Relay-guarantee logic, Logical full abstraction
      Bookmark

            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.

            Content

            Author and article information

            Contributors
            Conference
            September 2008
            September 2008
            : 259-247
            Affiliations
            [0001]Department of Computer Science

            Queen Mary, University of London
            [0002]Department of Computing

            Imperial College London
            Article
            10.14236/ewic/VOCS2008.22
            dad7801e-bdb8-48ba-9c82-a611e7b7ae36
            © Kohei Honda et al. Published by BCS Learning and Development Ltd. Visions of Computer Science - BCS International Academic Conference

            This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

            Visions of Computer Science - BCS International Academic Conference
            VOCS
            Imperial College, London, UK
            22 - 24 September 2008
            Electronic Workshops in Computing (eWiC)
            BCS International Academic Conference
            History
            Product

            1477-9358 BCS Learning & Development

            Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/VOCS2008.22
            Self URI (journal page): https://ewic.bcs.org/
            Categories
            Electronic Workshops in Computing

            Applied computer science,Computer science,Security & Cryptology,Graphics & Multimedia design,General computer science,Human-computer-interaction
            The π-calculus,Types,Hoare logics,Hennessy-Milner logics,Relay-guarantee logic,Logical full abstraction

            Comments

            Comment on this article