Paper: General Structural Operational Semantics through Categorical Logic (at LICS 2008)

Authors: Sam Staton

Abstract

Certain principles are fundamental to operational semantics, regardless of the languages or idioms involved. Such principles include rule-based definitions and proof techniques for congruenceresults. We formulate these principles in the general context of categorical logic. From this general formulation we recover precise results for particular language idioms by interpreting the logic inparticular categories. For instance, results for first-order calculi, such as CCS, arise from considering the general results in the category of sets. Results for languages involving substitution and name generation, such as the pi-calculus, arise from considering the general results in categories of sheaves and group actions. As an extended example, we develop a tyft/tyxt-like rule format for open bisimulation in the pi-calculus.

BibTeX

  @InProceedings{Staton-GeneralStructuralOp,
    author = 	 {Sam Staton},
    title = 	 {General Structural Operational Semantics through Categorical Logic},
    booktitle =  {Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science (LICS 2008)},
    year =	 {2008},
    month =	 {June}, 
    pages =      {166--177},
    location =   {Pittsburgh, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }