topic.rewrites_to_congruences.bib

@comment{{This file has been generated by bib2bib 1.99}}

@comment{{Command line: bibtex2html-1.99-with-magiclink/bib2bib -c topic:"rewrites_to_congruences" -ob topic.rewrites_to_congruences.bib sewellbib2.bib}}

@techreport{Sew98b,
  author = {Peter Sewell},
  title = {From Rewrite Rules to Bisimulation Congruences},
  institution = {University of Cambridge},
  year = {1998},
  optkey = {},
  opttype = {},
  number = {UCAM-CL-TR-444},
  optaddress = {},
  month = jun,
  note = {72pp. },
  pdf = {http://www.cl.cam.ac.uk/~pes20/labels-long.pdf},
  ps = {http://www.cl.cam.ac.uk/~pes20/labels-long.ps},
  pscmr = {http://www.cl.cam.ac.uk/~pes20/labels-long-cmr.ps},
  url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-444.html},
  abstract = {The dynamics of many calculi can be most clearly defined by a reduction semantics. To work with a calculus, however, an understanding of operational congruences is fundamental; these can often be given tractable definitions or characterisations using a labelled transition semantics. This paper considers calculi with arbitrary reduction semantics of three simple classes, firstly ground term rewriting, then left-linear term rewriting, and then a class which is essentially the action calculi lacking substantive name binding. General definitions of labelled transitions are given in each case, uniformly in the set of rewrite rules, and without requiring the prescription of additional notions of observation. They give rise to bisimulation congruences. As a test of the theory it is shown that bisimulation for a fragment of CCS is recovered. The transitions generated for a fragment of the Ambient Calculus of Cardelli and Gordon, and for SKI combinators, are also discussed briefly. },
  topic = {rewrites_to_congruences}
}

@inproceedings{Sew98a,
  author = {Peter Sewell},
  title = {From Rewrite Rules to Bisimulation Congruences},
  conf = {CONCUR 1998},
  booktitle = {Proceedings of Concurrency Theory (Nice). LNCS 1466},
  optcrossref = {},
  optkey = {},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  year = {1998},
  optorganization = {},
  publisher = {Springer-Verlag},
  optaddress = {},
  month = sep,
  pages = {269--284},
  note = {Subsumed by the TCS 2002 paper},
  optannote = {},
  url = {https://doi.org/10.1007/BFb0055628},
  doi = {10.1007/BFb0055628},
  pdf = {http://www.cl.cam.ac.uk/users/pes20/labels-medium.pdf},
  ps = {http://www.cl.cam.ac.uk/users/pes20/labels-medium.ps},
  abstract = {The dynamics of many calculi can be most clearly defined by a reduction semantics. To work with a calculus, however, an understanding of operational congruences is fundamental; these can often be given tractable definitions or characterisations using a labelled transition semantics. This paper considers calculi with arbitrary reduction semantics of three simple classes, firstly ground term rewriting, then left-linear term rewriting, and then a class which is essentially the action calculi lacking substantive name binding. General definitions of labelled transitions are given in each case, uniformly in the set of rewrite rules, and without requiring the prescription of additional notions of observation. They give rise to bisimulation congruences. As a test of the theory it is shown that bisimulation for a fragment of CCS is recovered. The transitions generated for a fragment of the Ambient Calculus of Cardelli and Gordon, and for SKI combinators, are also discussed briefly.},
  topic = {rewrites_to_congruences}
}

@article{Sew99a,
  author = {Peter Sewell},
  title = {From Rewrite Rules to Bisimulation Congruences},
  journal = {Theoretical Computer Science},
  year = {2002},
  optkey = {},
  volume = 274,
  number = {1--2},
  month = mar,
  pages = {183--230},
  note = {Invited submission for a CONCUR 98 special issue. },
  optannote = {},
  url = {http://dx.doi.org/10.1016/S0304-3975(00)00309-1},
  doi = {10.1016/S0304-3975(00)00309-1},
  pdf = {http://www.cl.cam.ac.uk/users/pes20/labels-tcs-final.pdf},
  ps = {http://www.cl.cam.ac.uk/users/pes20/labels-tcs-final.ps},
  abstract = {The dynamics of many calculi can be most clearly defined by a reduction semantics. To work with a calculus, however, an understanding of operational congruences is fundamental; these can often be given tractable definitions or characterisations using a labelled transition semantics. This paper considers calculi with arbitrary reduction semantics of three simple classes, firstly ground term rewriting, then left-linear term rewriting, and then a class which is essentially the action calculi lacking substantive name binding. General definitions of labelled transitions are given in each case, uniformly in the set of rewrite rules, and without requiring the prescription of additional notions of observation. They give rise to bisimulation congruences. As a test of the theory it is shown that bisimulation for a fragment of CCS is recovered. The transitions generated for a fragment of the Ambient Calculus of Cardelli and Gordon, and for SKI combinators, are also discussed briefly.},
  topic = {rewrites_to_congruences}
}