topic.observational_language_semantics.bib

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

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

@inproceedings{Sew97a,
  author = {Peter Sewell},
  title = {On Implementations and Semantics of a Concurrent Programming
                  Language},
  conf = {CONCUR 1997},
  booktitle = {Concurrency Theory (Warsaw). LNCS 1243},
  optcrossref = {},
  optkey = {},
  opteditor = {Antoni Mazurkiewicz and J{\'o}zef Winkowski},
  optvolume = {},
  optnumber = {},
  optseries = {},
  year = {1997},
  optorganization = {},
  publisher = {Springer-Verlag},
  optaddress = {},
  month = jul,
  pages = {391--405},
  pscmr = {http://www.cl.cam.ac.uk/~pes20/pict10-crc11ptcmr.ps},
  optannote = {},
  url = {https://doi.org/10.1007/3-540-63141-0},
  doi = {10.1007/3-540-63141-0},
  pdf = {http://www.cl.cam.ac.uk/users/pes20/pict9-crc11pt.pdf},
  ps = {http://www.cl.cam.ac.uk/users/pes20/pict9-crc11pt.ps},
  abstract = {The concurrency theory literature contains many proposals for models of process algebras. We consider an example application of the pi-calculus, the programming language Pict of Pierce and Turner, primarily in order to see how far it is possible to argue, from facts about the application, that some model is the most appropriate. We discuss informally the sense in which the semantics of Pict relates to the behaviour of actual implementations. Based on this we give an operational model of the interactions between a Pict implementation (considered as the abstract behaviour of a C program) and its environment (modelling an operating system and user). We then give a class of abstract machines and a definition of abstract machine correctness, using an adapted notion of testing, and prove that a sample abstract machine is indeed correct. We briefly discuss the standard of correctness appropriate for program transformations and the induced precongruence. Many of the semantic choices do indeed turn out to be determined by facts about Pict.},
  topic = {observational_language_semantics}
}