Nominal SOS

M. Cimini, M.R. Mousavi, M.A. Reniers, M.J. Gabbay

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    8 Citations (Scopus)
    39 Downloads (Pure)

    Abstract

    Plotkin's style of Structural Operational Semantics (SOS) has become a de facto standard in giving operational semantics to formalisms and process calculi. In many such formalisms and calculi, the concepts of names, variables and binders are essential ingredients. In this paper, we propose a formal framework for dealing with names in SOS. The framework is based on the Nominal Logic of Gabbay and Pitts and hence is called Nominal SOS. We define nominal bisimilarity, an adaptation of the notion of bisimilarity that is aware of binding. We provide evidence of the expressiveness of the framework by formulating the early pi-calculus and Abramsky's lazy lambda-calculus within Nominal SOS. For both calculi we establish the operational correspondence with the original calculi. Moreover, in the context of the pi-calculus, we prove that nominal bisimilarity coincides with Sangiorgi's open bisimilarity and in the context of the lambda-calculus we prove that nominal bisimilarity coincides with Abramsky's applicative bisimilarity.
    Original languageEnglish
    Title of host publication28th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2012, Bath, UK, June 6-9, 2012)
    PublisherENTCS
    Pages103-116
    DOIs
    Publication statusPublished - 2012
    Event28th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2012) - University of Bath, Bath, United Kingdom
    Duration: 6 Jun 20129 Jun 2012
    Conference number: 28
    http://dauns.math.tulane.edu/~mfps/MFPS28/MFPS28/MFPS_XXVIII.html

    Publication series

    NameElectronic Notes in Theoretical Computer Science
    Volume286
    ISSN (Print)1571-0061

    Conference

    Conference28th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2012)
    Abbreviated titleMFPS 2012
    CountryUnited Kingdom
    CityBath
    Period6/06/129/06/12
    Internet address

    Fingerprint Dive into the research topics of 'Nominal SOS'. Together they form a unique fingerprint.

    Cite this