<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%  These first few items are drafts, notes, variant bbl forms, etc - not to 
%  be included in the database
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


@InProceedings{Sew96-brief,
  author = 	 {Peter Sewell},
  title = 	 {Design Rules and Abstractions (from branching and
		  real time)},
  booktitle = 	 {Proceedings of  DCC 96: the 
3rd Workshop on Designing Correct Circuits
		  (B{\aa}stad, Sweden)},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTeditor =	 {S. Singh and M. Sheeran},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  series =	 {Electronic Workshops in Computing},
  year =	 {1996},
  OPTorganization = {},
  publisher =	 {Springer-Verlag},
  OPTaddress = 	 {},
  month =	 sep,
  OPTpages = 	 {},
  OPTnote =         {ISBN 3--540--76102--0. \fr},
  OPTannote = 	 {},
  url = "http://www.cl.cam.ac.uk/users/pes20/ab.ps"

}


@Misc{Sew99pi,
  OPTkey = 	 {},
  author =	 {Peter Sewell},
  title =	 {A Brief Introduction to Applied $\pi$},
  OPThowpublished = {},
  year =	 {1999},
  month =	 jan,
  note =	 {Lecture notes for the Mathfit Instructional Meeting on Recent Advances in 
Semantics and Types for Concurrency: Theory and Practice, July 1998.},
  OPTannote = 	 {},
  url = ""
}


@Misc{SW04,
  OPTkey =       {},
  author =       {Peter Sewell and Keith Wansbrough},
  title =        {Applied Semantics: Specifying and Developing Abstractions for Distributed Computation  (Grand Challenge Discussion Paper -- {GC2}, {GC4}, and {GC6})},
  howpublished = {Position paper for Grand Challenge meeting (Newcastle).  5pp},
  OPTmonth =     {},
  year =         {2004},
  OPTnote =      {},
  OPTannote =    {},
  url = ""
}


@Misc{netsem04a,
  OPTkey =       {},
  author =       {The Specification Team
(Steven Bishop and Matthew Fairbairn and Michael Norrish and Peter Sewell and Keith
Wansbrough)},
  title =        {The {TCP} Specification: A Quick Introduction},
  OPThowpublished = {},
  OPTmonth =     {},
  year =         {2004},
  OPTnote =      {},
  OPTannote =    {},
  url = ""
}


@Misc{SLWAZHV04-paper,
  author =       {Peter Sewell and
James J. Leifer and
Keith Wansbrough and
Mair Allen-Williams and
Zappa Nardelli, Francesco and
Pierre Habouzit and
Viktor Vafeiadis},
  title =        {Acute: High-level programming language design for distributed
computation},
  OPTinstitution =  {University of Cambridge Computer Laboratory},
  year =         {2004},
  OPTkey =       {},
  OPTtype =      {},
  OPTnumber =       {},
  OPTaddress =   {},
  OPTmonth =        {},
  note =         {Available from \url{http://www.cl.cam.ac.uk/users/pes20/acute/acute2-short.pdf}},
  OPTannote =    {},
  url = ""
}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% Everything that follows should be included in the database
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


@STRING(sv      = "Springer-Verlag" )


@Article{physics1,
  author = 	"G. F. Matthews and P. C. Stangeby and P. M. Sewell",
  title = 	"Investigation of the Wake Due to a Large Probe, using
		 a Spatially Scanning {L}angmuir Probe",
  journal = 	"J. Nucl. Mater.",
  year = 	"1987",
  volume = 	"145--147",
  OPTnumber = 	"",
  pages = 	"220--224",
  month = 	feb,
  note =         ""
}
@Article{physics2,
  author = 	"G. F. Matthews and G. M. McCracken and P. C. Stangeby
		 and C. S. Pitcher and
		 P. M. Sewell and D. H. J. Goodall",
  title = 	"The Optimisation of Limiter Geometry to Reduce
		 Impurity Influx in {T}okamaks",
  journal = 	"Plasma Physics and Controlled Fusion",
  year = 	"1987",
  volume = 	"29",
  number = 	"2",
  pages = 	"189--203",
  month = 	feb,
  note =         ""
}

@Article{physics3,
  author = 	"G. F. Matthews and G. M. McCracken and P. M. Sewell
		 and M. E. Woods and B. J. Hopkins",
  title = 	"The Determination of Sheath Potential from Retarding
		 Field Analyser Measurements in {T}okamak Edge Plasmas",
  journal = 	"J. Nucl. Mater.",
  year = 	"1987",
  volume = 	"145--147",
  OPTnumber = 	"",
  pages = 	"225--230",
  month = 	feb,
  note =         ""
}


@Article{physics4,
  author = 	"M. E. Woods and B. J. Hopkins and G. F. Matthews and
		 G. M. McCracken and
		 P. M. Sewell and H. Fahrang",
  title = 	"An Investigation of the Secondary-Electron Emission
		 of Carbon Samples Exposed to a Hydrogen Plasma",
  journal = 	"J. Physics D: Applied Physics",
  year = 	"1987",
  volume = 	"20",
  OPTnumber = 	"",
  pages = 	"1136--1142",
  OPTmonth = 	"",
  note =         ""
}


@InProceedings{Sew94,
  author = 	"Peter M. Sewell",
  title = 	"Bisimulation is Not Finitely (First-Order) Equationally Axiomatisable",
  booktitle = 	"Proceedings of LICS 94: the 9th IEEE Symposium on Logic in Computer Science (Paris)",
  year = 	"1994",
  OPTeditor = 	"",
  pages = 	"62--70",
  organization = 	"IEEE",
  OPTpublisher = 	"",
  OPTaddress = 	"",
  month =        jul,
  note =         "",
  OPTurl = "http://www.cl.cam.ac.uk/users/pes20/lics-nonax.ps"
}

@PhdThesis{Sew95,
  author = 	 "Peter Michael Sewell",
  title = 	 "The Algebra of Finite State Processes",
  school =       "University of Edinburgh",
  year = 	 "1995",
  OPTcrossref =  "",
  OPTkey = 	 "",
  OPTaddress = 	 "",
  month =	 oct,
  OPTtype = 	 "",
  note =	 "Dept. of Computer Science technical report CST-118-95, also published as LFCS-95-328",
  OPTannote = 	 "",
  url = "http://www.cl.cam.ac.uk/users/pes20/thesischarter.ps"
}


@InProceedings{Sew96b,
  author = 	 {Peter Sewell},
  title = 	 {Design Rules and Abstractions (from branching and
		  real time)},
  booktitle = 	 {Proceedings of the 
3rd Workshop on Designing Correct Circuits, DCC96,
		  B{\aa}stad, Sweden, September 1996},
  OPTcrossref =  {},
  OPTkey = 	 {},
  editor =	 {S. Singh and M. Sheeran},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  series =	 {Electronic Workshops in Computing},
  year =	 {1996},
  OPTorganization = {},
  publisher =	 sv,
  OPTaddress = 	 {},
  month =	 sep,
  OPTpages = 	 {},
  note =	 {ISBN 3--540--76102--0},
  OPTannote = 	 {},
  url = "http://www.cl.cam.ac.uk/users/pes20/ab.ps"
}

		  
@InProceedings{Sew97a,
  author = 	 {Peter Sewell},
  title = 	 {On Implementations and Semantics of a Concurrent Programming
                  Language},
  booktitle = 	 {Proceedings of CONCUR 97: Concurrency Theory (Warsaw). LNCS 1243},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTeditor =	 {Antoni Mazurkiewicz and J{\'o}zef Winkowski},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  year =	 {1997},
  OPTorganization = {},
  publisher =	 sv,
  OPTaddress = 	 {},
  month =        jul,
  pages =	 {391--405},
  note =         {},
  OPTannote = 	 {},
  url = "http://www.cl.cam.ac.uk/users/pes20/pict9-crc11pt.ps"
}

@Article{Sew97b,
  author = 	 {Peter Sewell},
  title = 	 {Nonaxiomatisability of Equivalences over Finite State 
                  Processes},
  journal = 	 {Annals of Pure and Applied Logic},
  year = 	 {1997},
  OPTkey = 	 {},
  volume =	 {90},
  OPTnumber = 	 {},
  month =        dec,
  pages =	 {163--191},
  note =         {Invited submittion from LICS '94},
  OPTannote = 	 {},
  url = "http://www.cl.cam.ac.uk/users/pes20/nonax.ps.gz",
}
		  

@InProceedings{Sew97d,
  author = 	 {Peter Sewell},
  title = 	 {Global/Local Subtyping and Capability Inference for a Distributed $\pi$-calculus},
  booktitle = 	 {Proceedings of ICALP '98: the 25th International Colloquium on Automata, Languages and Programming (Aalborg). LNCS 1443},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  year =	 {1998},
  OPTorganization = {},
  publisher =	 sv,
  OPTaddress = 	 {},
  month =	 jul,
  pages =	 {695--706},
  note =         {},
  OPTannote = 	 {},
  url = "http://www.cl.cam.ac.uk/users/pes20/globallocal-medium-cmr.ps"
}


@TechReport{Sew97c,
  author = 	 {Peter Sewell},
  title = 	 {Global/Local Subtyping for a Distributed $\pi$-calculus},
  institution =  {Computer Laboratory, University of Cambridge},
  year = 	 {1997},
  OPTkey = 	 {},
  OPTtype = 	 {},
  number =	 {UCAM-CL-TR-435},
  OPTaddress = 	 {},
  month =	 aug,
  note =       {57pp. },
  url = "http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-435.html"
}


@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. },
  url = "http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-444.html"
}

@InProceedings{Sew98a,
  author = 	 {Peter Sewell},
  title = 	 {From Rewrite Rules to Bisimulation Congruences},

  booktitle = 	 {Proceedings of CONCUR '98: Concurrency Theory (Nice). LNCS 1466},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTeditor =	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  year =	 {1998},
  OPTorganization = {},
  publisher =	 sv,
  OPTaddress = 	 {},
  month =	 sep,
  pages =	 {269--284},
  note =         {},
  OPTannote = 	 {},
  url = "http://www.cl.cam.ac.uk/users/pes20/labels-medium.ps"
}


@Article{Sew99a,
  author = 	 {Peter Sewell},
  title = 	 {From Rewrite Rules to Bisimulation Congruences},
  journal = 	 tcs,
  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://www.cl.cam.ac.uk/users/pes20/labels-tcs-final.ps"
}


@InProceedings{SWP98,
  author = 	 {Peter Sewell and Pawe{\l} T. Wojciechowski
                  and  Benjamin C. Pierce},
  title = 	 {Location Independence for Mobile Agents},
  booktitle = 	 {Proceedings of IFL 98: the Workshop on Internet Programming Languages (Chicago), in conjunction with ICCL},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  year =	 {1998},
  OPTorganization = {},
  OPTpublisher = {},
  OPTaddress = 	 {},
  month =	 may,
  note =        {6pp},
  OPTpages =        {6pp},
  OPTnote =         {},
  OPTannote = 	 {},
  url = "http://www.cl.cam.ac.uk/users/pes20/lima-draft.ps"
}


@TechReport{SWP99a,
  author = 	 {Peter Sewell and Pawe{\l} T. Wojciechowski
                  and  Benjamin C. Pierce},
  title = 	 {Location-Independent Communication for Mobile Agents: a Two-Level Architecture},
  institution =  {Computer Laboratory, University of Cambridge},
  year = 	 {1999},
  OPTkey = 	 {},
  OPTtype = 	 {},
  number =	 {UCAM-CL-TR-462},
  OPTaddress = 	 {},
  month =	 apr,
  note =         {31pp. },
  OPTannote = 	 {},
  url = "http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-462.html"
}

@InProceedings{SWP99b,
  author = 	 {Peter Sewell and Pawe{\l} T. Wojciechowski
                  and  Benjamin C. Pierce},
  title = 	 {Location-Independent Communication for Mobile Agents: a Two-Level Architecture},
  booktitle = 	 {Internet Programming Languages, LNCS 1686},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  year =	 {1999},
  OPTorganization = {},
  publisher =	 sv,
  OPTaddress = 	 {},
  month =	 oct,
  pages =	 {1--31},
  note =         {},
  OPTannote = 	 {},
  url = "http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-462.html"
}


@InProceedings{WS99,
  author = 	 {Pawe{\l} T. Wojciechowski and Peter Sewell},
  title = 	 {{N}omadic {P}ict: Language and Infrastructure Design for Mobile Agents},
  booktitle = 	 {Proceedings of ASA/MA 99: Agent Systems and Applications/Mobile Agents (Palm Springs)},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  year =	 {1999},
  OPTorganization = {},
  OPTpublisher = {},
  OPTaddress = 	 {},
  month =	 oct,
  pages =	 {2--12},
  note =         {Best paper award. },
  OPTannote = 	 {},
  url = "http://www.cl.cam.ac.uk/users/pes20/asama.ps"
}

@Article{WS00,
  author = 	 {Pawe{\l} T. Wojciechowski and Peter Sewell},
  title = 	 {{N}omadic {P}ict: Language and Infrastructure Design for Mobile Agents},
  journal = 	 {{IEEE} {C}oncurrency},
  year = 	 {2000},
  OPTkey = 	 {},
  volume =       {8},
  number =       {2},
  month =        {April--June},
  pages =        {42--52},
  note =	 {Invited submission for ASA/MA 99. },
  OPTannote = 	 {},
  url = ""
}

@InProceedings{US01,
  author =       {Asis Unyapoth and Peter Sewell},
  title =        {Nomadic {P}ict: Correct Communication Infrastructure for Mobile Computation},
  booktitle =    {Proceedings of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (London)},
  OPTcrossref =  {},
  OPTkey =       {},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  year =         {2001},
  OPTorganization = {},
  OPTpublisher = {},
  OPTaddress =   {},
  month =        jan,
  pages =        {116--127},
  note =         {},
  OPTannote =    {},
  url = "http://www.cl.cam.ac.uk/users/pes20/nproofs-popl.ps"
}


@TechReport{SV99a,
  author = 	 {Peter Sewell and Jan Vitek},
  title = 	 {Secure Composition of Insecure Components},
  institution =  {Computer Laboratory, University of Cambridge},
  year = 	 {1999},
  OPTkey = 	 {},
  OPTtype = 	 {},
  number =	 {UCAM-CL-TR-463},
  OPTaddress = 	 {},
  month =	 apr,
  note =         {44pp. },
  OPTannote = 	 {},
  url = "http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-463.html"
}


@InProceedings{SV99b,
  author = 	 {Peter Sewell and Jan Vitek},
  title = 	 {Secure Composition of Insecure Components},
  booktitle = 	 {Proceedings of CSFW 99: the 12th IEEE Computer Security Foundations Workshop (Mordano)},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  year =	 {1999},
  OPTorganization = {},
  publisher =	 {IEEE Computer Society},
  OPTaddress = 	 {},
  month =	 jun,
  pages =	 {136--150},
  note =         {},
  OPTannote = 	 {},
  url = "http://www.cl.cam.ac.uk/users/pes20/wrap-csfw.ps"
}


@TechReport{SV99c,
  author = 	 {Peter Sewell and Jan Vitek},
  title = 	 {Secure Composition of Untrusted Code:
Wrappers and Causality Types},
  institution =  {Computer Laboratory, University of Cambridge},
  year = 	 {1999},
  OPTkey = 	 {},
  OPTtype = 	 {},
  number =	 {UCAM-CL-TR-478},
  OPTaddress = 	 {},
  month =	 nov,
  note =       {36pp. },
  url = "http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-478.html"
}


@Article{SV-jcs,
  author = 	 {Peter Sewell and Jan Vitek},
  title = 	 {Secure Composition of Untrusted Code: Box-$\pi$, Wrappers and Causality Types},
  journal =      {Journal of Computer Security},
  year =         {2003},
  OPTkey =       {},
  volume =       {11},
  number =       {2},
  OPTmonth =     {},
  pages =        {135-188},
  note =         {Invited submission for a CSFW 00 special issue.},
  OPTannote =    {},
  url = "http://www.cl.cam.ac.uk/users/pes20/wrapall.ps"
}


@InProceedings{SV00a,
  author = 	 {Peter Sewell and Jan Vitek},
  title = 	 {Secure Composition of Untrusted Code: Wrappers and Causality Types},
  booktitle = 	 {Proceedings of CSFW 00: the 13th IEEE Computer Security Foundations Workshop (Cambridge)},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  year =	 {2000},
  OPTorganization = {},
  publisher =	 {IEEE Computer Society},
  OPTaddress = 	 {},
  month =	 jul,
  pages =        {269--284},
  note =         {},
  OPTannote = 	 {},
  url = "http://www.cl.cam.ac.uk/users/pes20/wraptypes.ps"
}


@TechReport{Sew00pi-tr,
  author =       {Peter Sewell},
  title =        {Applied $\pi$ -- A Brief Tutorial},
  institution =  {Computer Laboratory, University of Cambridge},
  year =         {2000},
  OPTkey =       {},
  OPTtype =      {},
  number =       {UCAM-CL-TR-498},
  OPTaddress =   {},
  month =        aug,
  note =         {65pp. },
  OPTannote =    {},
  url = "http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-498.html"
}


@Misc{Sew00pi,
  author = 	 {Peter Sewell},
  title = 	 {Chapter 9, {P}i {C}alculus,  in the book {F}ormal {M}ethods for {D}istributed {P}rocessing, {A} {S}urvey of {O}bject {O}riented
{A}pproaches, edited by {H}oward {B}owman and {J}ohn {D}errick},
  publisher = 	 {Cambridge University Press},
  year =         {2001},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  month =        dec,
  pages =        {177--197},
  OPTtype = 	 {},
  OPTnote =	 {ISBN: 0521771846},
  OPTannote = 	 {},
  url = ""
}


@InProceedings{CS00,
  author = 	 {Gian Luca Cattani and Peter Sewell},
  title = 	 {Models for Name-Passing Processes: Interleaving and Causal (Extended Abstract)},
  booktitle = 	 {Proceedings of LICS 2000: the 15th IEEE Symposium on Logic in Computer Science (Santa Barbara) },
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  year =	 {2000},
  OPTorganization = {},
  OPTpublisher = {},
  OPTaddress = 	 {},
  month =	 jun,
  pages =        {322--333},
  note =         {},
  OPTannote = 	 {},
  url = "http://www.cl.cam.ac.uk/users/pes20/indexing.ps"

}


@TechReport{CS00b,
  author = 	 {Gian Luca Cattani and Peter Sewell},
  title = 	 {Models for Name-Passing Processes: Interleaving and Causal},
  institution =  {Computer Laboratory, University of Cambridge},
  year =         {2000},
  OPTkey =       {},
  OPTtype =      {},
  number =       {UCAM-CL-TR-505},
  OPTaddress =   {},
  month =        sep,
  note =         {42pp. },
  OPTannote =    {},
  url = "http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-505.html"
}


@Article{CS00c,
  author = 	 {Gian Luca Cattani and Peter Sewell},
  title = 	 {Models for Name-Passing Processes: Interleaving and Causal},
  journal =      {Information and Computation},
  year =         {2004},
  OPTkey =       {},
  volume =       {190},
  number =       {2},
  pages =        {136--178},
  month =        may,
  OPTnote =         {},
  OPTannote =    {},
  url = ""
}


@TechReport{Sew00,
  author =       {Peter Sewell},
  title =        {Modules, Abstract Types, and Distributed Versioning},
  institution =  {University of Cambridge},
  year =         {2000},
  OPTkey =       {},
  OPTtype =      {},
  number =       {UCAM-CL-TR-506},
  OPTaddress =   {},
  month =        sep,
  note =         {46pp. },
  OPTannote =    {},
  url = "http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-506.html"

}


@InProceedings{Sew01a,
  author =       {Peter Sewell},
  title =        {Modules, Abstract Types, and Distributed Versioning},
  booktitle =    {Proceedings of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (London)},
  OPTcrossref =  {},
  OPTkey =       {},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  year =         {2001},
  OPTorganization = {},
  OPTpublisher = {},
  OPTaddress =   {},
  month =        jan,
  pages =        {236--247},
  note =         {},
  OPTannote =    {},
  url = "http://www.cl.cam.ac.uk/users/pes20/versions-popl.pdf"
}


@TechReport{SSW01b,
  author =       {Andrei Serjantov and Peter Sewell and Keith Wansbrough},
  title =        {The {UDP} Calculus: Rigorous Semantics for Real Networking},
  institution =  {Computer Laboratory, University of Cambridge},
  year =         {2001},
  OPTkey =       {},
  OPTtype =      {},
  number =       {UCAM-CL-TR-515},
  OPTaddress =   {},
  month =        jul,
  note =         {iv+70pp. },
  url = "http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-515.html"

}

@InProceedings{SSW01a,
  author =       {Andrei Serjantov and Peter Sewell and Keith Wansbrough},
  title =        {The {UDP} Calculus: Rigorous Semantics for Real Networking},
  booktitle =    {Proceedings of TACS 2001: Theoretical Aspects of Computer Software (Sendai), LNCS 2215},
  OPTcrossref =  {},
  OPTkey =       {},
  pages =        {535--559},
  year =      {2001},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  month =        oct,
  OPTorganization = {},
  OPTpublisher = {},
  note =         {},
  OPTannote =    {},
  url = "http://www.cl.cam.ac.uk/users/pes20/Netsem/udp-short.ps"
}


@Misc{SWN01,
  OPTkey =       {},
  author =       {Peter Sewell and Keith Wansbrough and Michael Norrish},
  title =        {Timing {UDP}: The {HOL} Model},
  howpublished = {Available from \url{http://www.cl.cam.ac.uk/users/pes20/Netsem/index.html}},
  month =        jul,
  year =         {2001},
  OPTnote =      {},
  OPTannote =    {}
}


@InProceedings{WNSS01,
  author =       {Keith Wansbrough and Michael Norrish and Peter Sewell and Andrei Serjantov},
  title =        {Timing {UDP}: mechanized semantics for sockets, threads and failures},
  booktitle =    {Proceedings of ESOP 2002: the 11th European Symposium on Programming (Grenoble), LNCS 2305},
  OPTcrossref =  {},
  OPTkey =       {},
  pages =        {278--294},
  year =         {2002},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  month =        apr,
  OPTorganization = {},
  OPTpublisher = {},
  note =         {},
  OPTannote =    {},
  url = "http://www.cl.cam.ac.uk/users/pes20/Netsem/timing-udp-a4.ps"
}


@InProceedings{NSW02,
  author =       {Michael Norrish and Peter Sewell and Keith Wansbrough},
  title =        {Rigour is good for you, and feasible: reflections on formal treatments of {C} and {UDP} sockets. },
  booktitle =    {Proceedings of the 10th ACM SIGOPS European Workshop (Saint-Emilion)},
  OPTcrossref =  {},
  OPTkey =       {},
  pages =        {49--53},
  year =         {2002},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  month =        sep,
  OPTorganization = {},
  OPTpublisher = {},
  note =         {},
  OPTannote =    {},
  url = "http://www.cl.cam.ac.uk/users/pes20/Netsem/sigops-ew2002.ps"
}

@TechReport{BS03,
  author = 	 {G. M. Bierman and P. Sewell},
  title = 	 {Iota: A concurrent {XML} scripting language with applications to Home Area Networking},
  institution =  {Computer Laboratory, University of Cambridge},
  year = 	 {2003},
  OPTkey = 	 {},
  OPTtype = 	 {},
  number =	 {UCAM-CL-TR-557},
  OPTaddress = 	 {},
  month =	 jan,
  note =       {32pp. },
  url = "http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-557.html"
}


@InProceedings{BHSS03,
  author =       {Gavin Bierman and Michael Hicks and Peter Sewell and Gareth Stoyle},
  title =        {Formalizing Dynamic Software Updating},
  booktitle =    {Proceedings of USE 2003: the Second International Workshop on Unanticipated Software
                                            Evolution (Warsaw), in conjunction with ETAPS},
  OPTcrossref =  {},
  OPTkey =       {},
  OPTpages =     {},
  year =         {2003},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  month =        apr,
  OPTorganization = {},
  OPTpublisher = {},
  note =         {17pp},
  OPTannote =       {},
  url = "http://www.cl.cam.ac.uk/users/pes20/formalUpdate.ps"
}


@InProceedings{BHSSW03,
  author =       {Gavin Bierman and Michael Hicks and Peter Sewell and Gareth Stoyle and Keith Wansbrough},
  title =        {Dynamic Rebinding for Marshalling and Update, with Destruct-time lambda},
  booktitle =    {Proceedings of ICFP 2003: the 8th ACM SIGPLAN International Conference on Functional Programming (Uppsala)},
  OPTcrossref =  {},
  OPTkey =       {},
  pages =        {99--110},
  year =         {2003},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  month =        aug,
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote =         {},
  OPTannote =    {},
  url = "http://www.cl.cam.ac.uk/users/pes20/dynbind2-short.ps"
}


@InProceedings{LPSW03,
  author =       {James Leifer and Gilles Peskine and Peter Sewell and Keith Wansbrough},
  title =        {Global abstraction-safe marshalling with hash types},
  booktitle =    {Proceedings of ICFP 2003: the 8th ACM SIGPLAN International Conference on Functional Programming (Uppsala)},
  OPTcrossref =  {},
  OPTkey =       {},
  pages =        {87--98},
  year =         {2003},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  month =        aug,
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote =         {},
  OPTannote =    {},
  url = "http://www.cl.cam.ac.uk/users/pes20/hashtypes.ps"
}


@TechReport{LPSW03-tr,
  author =       {James Leifer and Gilles Peskine and Peter Sewell and Keith Wansbrough},
  title =        {Global abstraction-safe marshalling with hash types},
  institution =  {University of Cambridge Computer Laboratory},
  year =         {2003},
  OPTkey =       {},
  OPTtype =      {},
  number =       {UCAM-CL-TR-569},
  OPTaddress =   {},
  month =        jun,
  note =         {Also published as INRIA Rocquencourt report RR-4851. 86pp.},
  OPTannote =    {},
  url = "http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-569.html"
}


@TechReport{BHSSW04-tr,
  author =       {Gavin Bierman and Michael Hicks and Peter Sewell and Gareth Stoyle and Keith Wansbrough},
  title =        {Dynamic Rebinding for Marshalling and Update, with Destruct-time $\lambda$},
  institution =  {University of Cambridge Computer Laboratory},
  year =         {2004},
  OPTkey =       {},
  OPTtype =      {},
  number =       {UCAM-CL-TR-568},
  OPTaddress =   {},
  month =        feb,
  note =         {85pp},
  OPTannote =    {},
  url = "http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-568.html"
}

@InProceedings{SS03,
  author =       {Andrei Serjantov and Peter Sewell},
  title =        {Passive Attack Analysis for Connection-Based Anonymity Systems},
  booktitle =    {Proceedings of ESORICS 2003:  the 8th European Symposium on Research in Computer Security (Gj{\o}vik), LNCS 2808},
  OPTcrossref =  {},
  OPTkey =       {},
  pages =        {116--131},
  year =         {2003},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  month =        oct,
  OPTorganization = {},
  OPTpublisher = {},
  note =         {},
  OPTannote =    {},
  url = "http://www.cl.cam.ac.uk/users/pes20/conn_sys.ps"
}


@Article{SS05,
  author =       {Andrei Serjantov and Peter Sewell},
  title =        {Passive-attack analysis for connection-based anonymity systems},
  journal =      {International Journal of Information Security},
  year =         {2005},
  OPTkey =       {},
  volume =       {4},
  number =       {3},
  pages =        {172--180},
  month =        jun,
  OPTnote =      {Special issue on ESORICS 2003},
  OPTannote =    {},
  url = ""
}

@InProceedings{BS04a,
  author =       {Moritz Y. Becker and Peter Sewell},
  title =        {Cassandra: Distributed Access Control Policies with Tunable Expressiveness},
  OPTcrossref =  {},
  OPTkey =       {},
  booktitle =    {Proceedings of POLICY 2004: the 5th IEEE International Workshop on Policies for Distributed Systems and Networks (Yorktown Heights)},
  OPTpages =     {},
  year =         {2004},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  month =        jun,
  OPTorganization = {},
  OPTpublisher = {},
  note =         {},
  OPTannote =    {},
  url = "http://www.cl.cam.ac.uk/users/pes20/policy-policy04.pdf"
}


@InProceedings{BS04b,
  author =       {Moritz Y. Becker and Peter Sewell},
  title =        {Cassandra: Flexible Trust Management, Applied to Electronic Health Records},
  OPTcrossref =  {},
  OPTkey =       {},
  booktitle =    {Proceedings of CSFW 2004: the 17th IEEE Computer Security Foundations Workshop (Asilomar)},
  pages =        {139--154},
  year =         {2004},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  month =        jun,
  OPTorganization = {},
  OPTpublisher = {},
  note =         {},
  OPTannote =    {},
  url = "http://www.cl.cam.ac.uk/users/pes20/policy-csfw04.ps"
}


@InProceedings{LNSW04,
  author =       {James Leifer and Michael Norrish and Peter  Sewell and Keith Wansbrough},
  title =        {Acute and {TCP}: specifying and developing abstractions for global computation},
  OPTcrossref =  {},
  OPTkey =       {},
  booktitle =    {Proceedings of the APPSEM II Workshop (Tallinn)},
  pages =        {},
  year =         {2004},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  month =        apr,
  OPTorganization = {},
  OPTpublisher = {},
  note =         {2pp},
  OPTannote =    {},
  url = ""
}


@TechReport{SLWAZHV04,
  author =       {Peter Sewell and
James J. Leifer and
Keith Wansbrough and
Mair Allen-Williams and
Zappa Nardelli, Francesco and
Pierre Habouzit and
Viktor Vafeiadis},
  title =        {Acute: High-level programming language design for distributed
computation. Design rationale and language definition},
  institution =  {University of Cambridge Computer Laboratory},
  year =         {2004},
  OPTkey =       {},
  OPTtype =      {},
  number =       {UCAM-CL-TR-605},
  OPTaddress =   {},
  month =        oct,
  note =         {Also published as INRIA RR-5329. 193pp},
  OPTannote =    {},
  url = "http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-605.html"
}


@InProceedings{SLWZAHV05,
  author =       {Peter Sewell and
James J. Leifer and
Keith Wansbrough and
Zappa Nardelli, Francesco and
Mair Allen-Williams and
Pierre Habouzit and
Viktor Vafeiadis},
  title =        {Acute: High-level programming language design for distributed
computation},
  OPTcrossref =  {},
  OPTkey =       {},
  booktitle =    {Proceedings of ICFP 2005: the 10th ACM SIGPLAN International Conference on
Functional Programming (Tallinn)},
  pages =        {15--26},
  year =         {2005},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  month =        sep,
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote =         {},
  OPTannote =    {},
  url = "http://www.cl.cam.ac.uk/users/pes20/acute/acute2-short.ps"
}

@Misc{SLWAZHV05-release-0-50-1,
  author =       {Peter Sewell and
James J. Leifer and
Keith Wansbrough and
Mair Allen-Williams and
Zappa Nardelli, Francesco and
Pierre Habouzit and
Viktor Vafeiadis},
  title =        {Source release of the {Acute} system},
  OPTinstitution =  {University of Cambridge Computer Laboratory},
  year =         {2005},
  OPTkey =       {},
  OPTtype =      {},
  OPTnumber =       {},
  OPTaddress =   {},
  month =        jan,
  note =         {Available from \url{http://www.cl.cam.ac.uk/users/pes20/acute/distro/acute-0.50-1-src.tar.gz}},
  OPTannote =    {},
  url = "http://www.cl.cam.ac.uk/users/pes20/acute/distro/acute-0.50-1-src.tar.gz"
}


@InProceedings{SHBSN05,
  author =       {Gareth Stoyle and
Michael Hicks and
Gavin Bierman and
Peter Sewell and
Iulian Neamtiu},
  title =        {\textit{Mutatis Mutandis}: Safe and Predictable Dynamic Software Updating},
  OPTcrossref =  {},
  OPTkey =       {},
  booktitle =    {Proceedings of POPL 2005: The 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Long Beach)},
  pages =        {183--194},
  year =         {2005},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  month =        jan,
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote =         {},
  OPTannote =    {},
  url = "http://www.cl.cam.ac.uk/users/pes20/update-popl-2005.pdf"
}


@InProceedings{TCP:paper,
  OPTkey =       {},
  author =       {Steven Bishop and Matthew Fairbairn and Michael Norrish and
Peter Sewell and Michael Smith and Keith Wansbrough},
  title =        {Rigorous specification and conformance testing techniques for network protocols, as applied to {TCP}, {UDP}, and {S}ockets},
  year =         {2005},
  OPTnote =         {12pp},
  OPTcrossref =  {},
  OPTkey =       {},
  booktitle =    {Proceedings of SIGCOMM 2005: ACM Conference on Computer Communications (Philadelphia), \emph{published as Vol.~35, No.~4 of} {{Computer Communication Review}}},
  pages =        {265--276},
  OPTyear =      {},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  month =        aug,
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote =         {},
  OPTannote =    {},
  url = "http://www.cl.cam.ac.uk/users/pes20/Netsem/paper.ps",
}


@TechReport{TCP:tr,
  OPTkey =       {},
  author =       {Steven Bishop and Matthew Fairbairn and Michael Norrish and
Peter Sewell and Michael Smith and Keith Wansbrough},
  title =        {{TCP}, {UDP}, and {S}ockets: rigorous and experimentally-validated
behavioural specification. {V}olume 1: Overview},
  institution =  {Computer Laboratory, University of Cambridge},
  number      = {UCAM-CL-TR-624},
  note = {88pp},
  OPTnote = {Available at \url{http://www.cl.cam.ac.uk/users/pes20/Netsem/}},
  month =        mar,
  year =         {2005},
  OPTannote =    {},
  url = "http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-624.html"
}


@TechReport{TCP:spec,
  OPTkey =       {},
  author =       {Steven Bishop and Matthew Fairbairn and Michael Norrish and
Peter Sewell and Michael Smith and Keith Wansbrough},
  title =        {{TCP}, {UDP}, and {S}ockets: rigorous and experimentally-validated
behavioural specification. {V}olume 2: The
Specification.},
  institution =  {Computer Laboratory, University of Cambridge},
  number      = {UCAM-CL-TR-625},
  note = {386pp},
  OPTnote={ Available at \url{http://www.cl.cam.ac.uk/users/pes20/Netsem/}},
  month =        mar,
  year =         {2005},
  OPTannote =    {},
  url = "http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-625.html"
}


@InProceedings{TCP:techpaper,
  OPTkey =       {},
  author =       {Steven Bishop and Matthew Fairbairn and Michael Norrish and
Peter Sewell and Michael Smith and Keith Wansbrough},
  title =        {Engineering with Logic: {HOL} Specification and Symbolic-Evaluation Testing for {TCP} Implementations},
  year =         {2006},
  pages =         {55--66},
  OPTcrossref =  {},
  OPTkey =       {},
  booktitle =    {Proceedings of POPL 2006: The 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Charleston)},
  OPTpages =     {},
  OPTyear =      {},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  month =        jan,
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote =         {To appear.},
  OPTannote =    {},
  url = "http://www.cl.cam.ac.uk/users/pes20/Netsem/tech-paper.ps"
}


@InProceedings{poplmark,
  AUTHOR = {Brian E. Aydemir and Aaron Bohannon and Matthew Fairbairn
                  and J. Nathan Foster and Benjamin C. Pierce and Peter
                  Sewell and Dimitrios Vytiniotis and Geoffrey Washburn and
                  Stephanie Weirich and Steve Zdancewic},
  TITLE = {Mechanized metatheory for the masses: {T}he {POPL}mark
                  {C}hallenge},
  YEAR = 2005,
  MONTH = aug,
  OPTcrossref =  {},
  OPTkey =       {},
  booktitle =    {Proceedings of TPHOLs 2005: the 18th International Conference on Theorem Proving in Higher Order Logics (Oxford), LNCS 3603},
  pages =        {50--65},
  OPTyear =      {},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  OPTmonth =     {},
  OPTorganization = {},
  OPTpublisher = {},
  note =         {},
  OPTannote =    {},
  url = "http://www.cis.upenn.edu/group/proj/plclub/mmm/poplmark/poplmark.pdf"
}


@InProceedings{PSWZ05,
   author =     {Benjamin C. Pierce and Peter Sewell and
                   Stephanie Weirich and Steve Zdancewic},
   title =       {It is Time to Mechanize Programming
                 Language Metatheory},
   booktitle =  {Verified Software: Theories, Tools, Experiments (Z\"urich)},
   year =       2005,
   OPTaddress =    {, Switzerland},
   month =      oct,
   note =       {5pp},
   optnote =       {This position paper is adapted from
                   the introduction
                   to the POPLMark Challenge paper~\cite{poplmark}. 5pp},
   pdf = {http://vstte.ethz.ch/Files/pierce-sewell-weirich-zdancewic.pdf}
}


@InProceedings{BSSS06,
  author =       {John Billings and Peter Sewell and Mark Shinwell and Rok Strni\v sa},
  title =        {Type-Safe Distributed Programming for {OCaml}},
  OPTcrossref =  {},
  OPTkey =       {},
  booktitle =    {Proceedings of ML'06, the 2006 ACM SIGPLAN Workshop on ML},
  pages =        {20--31},
  year =         {2006},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  month =        sep,
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote =         {To appear},
  OPTannote =    {}
}

@InProceedings{BDJRS06,
  author =       {Adam Biltcliffe and Michael Dales and Sam Jansen and Thomas Ridge and Peter Sewell},
  title =        {Rigorous Protocol Design in Practice: An Optical Packet-Switch {MAC} in {HOL}},
  OPTcrossref =  {},
  OPTkey =       {},
  booktitle =    {Proceedings of ICNP, the 14th IEEE International Conference on Network Protocols (Santa Barbara)},
  OPTpages =     {},
  year =         {2006},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  month =        nov,
  OPTorganization = {},
  OPTpublisher = {},
  note =         {10pp},
  OPTannote =    {}
}


@Article{SHBSN-toplas,
 author = {Gareth Stoyle and Michael Hicks and Gavin Bierman and Peter Sewell and Iulian Neamtiu},
 title = {Mutatis Mutandis: Safe and predictable dynamic software updating},
 journal = {ACM Trans. Program. Lang. Syst.},
 volume = {29},
 number = {4},
 year = {2007},
 issn = {0164-0925},
 pages =         {70pp},
 note = {70pp},
 doi = {http://doi.acm.org/10.1145/1255450.1255455},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 }


@article{1255455,
 author = {Gareth Stoyle and Michael Hicks and Gavin Bierman and Peter Sewell and Iulian Neamtiu},
 title = {Mutatis Mutandis: Safe and predictable dynamic software updating},
 journal = {ACM Trans. Program. Lang. Syst.},
 volume = {29},
 number = {4},
 year = {2007},
 issn = {0164-0925},
 pages = {70pp},
 doi = {http://doi.acm.org/10.1145/1255450.1255455},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 }


@Article{SLWZAHV-jfp,
  author =       {Peter Sewell and
James J. Leifer and
Keith Wansbrough and
Zappa Nardelli, Francesco and
Mair Allen-Williams and
Pierre Habouzit and
Viktor Vafeiadis},
  title =        {Acute: High-level programming language design for distributed
computation},
  journal =      {J. Functional Programming},
  optjournal =      {Journal of Functional Programming},
  year =         {2007},
  OPTkey =       {},
  volume =       {17},
  number =       {4--5},
  pages =        {547--612},
  month =        jul,
  note =         {Invited submission for an ICFP 2005 special issue},
  OPTannote =    {}
}

@Article{BHSSW-jfp,
  author =       {Peter Sewell and Gareth Stoyle and Michael Hicks and Gavin Bierman and Keith Wansbrough},
  title =        {Dynamic Rebinding for Marshalling and Update, via Redex-time and  Destruct-time Reduction},
  journal =      {Journal of Functional Programming},
  year =         {2008},
  OPTkey =       {},
  volume =       {18},
  number =       {4},
  pages =        {437--502},
  OPTmonth =     {},
  note =         {66pp.},
  OPTannote =    {}
}


@InProceedings{ljam-sub,
  author =       {Rok {Strni\v sa} and Peter Sewell and Matthew Parkinson},
  title =        {The {J}ava {M}odule {S}ystem: core design and semantic definition},
  OPTcrossref =  {},
  OPTkey =       {},
  booktitle =    {Proceedings of {OOPSLA} 2007, the {22nd ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages and Applications (Montre{\'a}l)}},
  optpages =        {15 pp},
  note =        {15pp},
  year =         {2007},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  month =        oct,
  OPTorganization = {},
  OPTpublisher = {},
  OPTannote =    {}
}

@InProceedings{ott-sub,
  author =       {Peter Sewell and Zappa Nardelli, Francesco  and Scott Owens and Gilles Peskine and Thomas Ridge and Susmit Sarkar and Rok Strni\v sa},
  title =        {{Ott}: Effective Tool Support for the Working Semanticist},
  OPTcrossref =  {},
  OPTkey =       {},
  booktitle =    {Proceedings of ICFP 2007:  {the 12th ACM SIGPLAN International Conference on Functional Programming (Freiburg)}},
  optpages =        {12pp},
  note =        {12pp},
  year =         {2007},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  month =        oct,
  OPTorganization = {},
  OPTpublisher = {},
  optnote =         {To appear},
  OPTannote =    {}
}

@article{ott-jfp,
  author =       {Peter Sewell and Zappa Nardelli, Francesco  and Scott Owens and Gilles Peskine and Thomas Ridge and Susmit Sarkar and Rok Strni\v sa},
  title =        {{Ott}: Effective Tool Support for the Working Semanticist},
  OPTcrossref =  {},
  OPTkey =       {},
  optjournal =      {J. Functional Programming},
  journal =      {Journal of Functional Programming},
  year =         {2010},
  OPTkey =       {},
  volume =       {20},
  number =       {1},
  pages =        {70--122},
  month =        jan,
  note =         {Invited submission from ICFP 2007},
  OPTannote =    {}
}


@Misc{acute-release,
  OPTkey =       {},
  author =       {Peter Sewell and
James J. Leifer and
Keith Wansbrough and
Mair Allen-Williams and
Zappa Nardelli, Francesco and
Pierre Habouzit and
Viktor Vafeiadis},
  title =        {The {Acute} Language Implementation.  Source release 0.50-1.},
  howpublished = {\url{http://www.cl.cam.ac.uk/users/pes20/acute/index.html}},
  month =        jan,
  year =         {2005},
  OPTnote =      {},
  OPTannote =    {}
}


@Misc{udp-model,
  OPTkey =       {},
  author =       {Michael Norrish and Andrei Serjantov and Peter Sewell and Keith Wansbrough},
  title =        {Timing {UDP}: The {HOL} Model},
  OPThowpublished = {},
  month =        jul,
  year =         {2001},
  note =         {\url{http://www.cl.cam.ac.uk/users/pes20/Netsem/index.html}},
  OPTannote =    {}
}


@Misc{hashcaml-release,
  OPTkey =       {},
  author =       {John Billings and Peter Sewell and Mark Shinwell and Rok Strni\v sa},
  title =        {{HashCaml} release, version 3.09.1-alpha-795},
  OPThowpublished = {},
  month =        apr,
  year =         {2006},
  note =      {\url{http://www.cl.cam.ac.uk/~pes20/hashcaml/index.html}},
  OPTannote =    {}
}

@Misc{ott-release,
  OPTkey =       {},
  author =       {Peter Sewell and Zappa Nardelli, Francesco },
  title =        {Ott release, version 0.10.9},
  OPThowpublished = {},
  month =        aug,
  year =         {2007},
  note =      {\url{http://www.cl.cam.ac.uk/~pes20/ott/}},
  OPTannote =    {}
}

@InProceedings{SSZ07,
  author =       {Susmit Sarkar and Peter Sewell and Zappa Nardelli, Francesco},
  title =        {Specifying real-world binding structures},
  OPTcrossref =  {},
  OPTkey =       {},
  booktitle =    {2nd Informal ACM SIGPLAN Workshop on Mechanizing Metatheory
(Freiburg), in conjunction with ICFP},
  OPTpages =     {},
  year =         {2007},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  month =        oct,
  OPTorganization = {},
  OPTpublisher = {},
  note =         {1pp},
  OPTannote =    {}
}

@article{DBLP:journals/entcs/Sewell06,
  author    = {Peter Sewell},
  title     = {Process Calculi: The End of the Beginning? (From Thought
               Experiments to Experimental Semantics)},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {162},
  year      = {2006},
  pages     = {317-321},
  ee        = {http://dx.doi.org/10.1016/j.entcs.2006.01.033},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@InProceedings{RNS08,
  author =       {Tom Ridge and Michael Norrish and Peter Sewell},
  title =        {A rigorous approach to networking: {TCP}, from implementation to protocol to service},
  OPTcrossref =  {},
  OPTkey =       {},
  booktitle =    {Proc.~FM'08: 15th International Symposium on Formal Methods (Turku, Finland), LNCS 5014},
  pages =        {294--309},
  year =         2008,
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  month =        may,
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote =         {To appear},
  OPTannote =    {}
}


@InProceedings{x86popl,
  OPTkey =       {},
  author =       {S. Sarkar and P. Sewell and Zappa Nardelli, F. and S. Owens and T. Ridge and T. Braibant and M. Myreen and J. Alglave},
  OPTauthor =       {Susmit Sarkar and Peter Sewell and Zappa Nardelli, Francesco and Scott Owens and Tom Ridge and Thomas Braibant and Magnus Myreen and Jade Alglave},
  title =        {The Semantics of {x86-CC} Multiprocessor Machine Code},
  year =         {2009},
  OPTpages =         {},
  OPTcrossref =  {},
  OPTkey =       {},
  booktitle =    {Proc.~POPL 2009},
  OPTpages =     {},
  OPTyear =      {},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  month =        jan,
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote =         {To appear},
  OPTannote =    {},
  OPTurl = ""
}


@InProceedings{damp09,
  OPTkey =       {},
  author =       {Jade Alglave and Anthony Fox and Samin Ishtiaq and Magnus O. Myreen and Susmit Sarkar and Peter Sewell and Zappa Nardelli, Francesco},
  title =        {The Semantics of {Power} and {ARM} Multiprocessor Machine Code},
  year =         {2009},
  OPTpages =         {},
  OPTcrossref =  {},
  OPTkey =       {},
  booktitle =    {DAMP 2009: Workshop on
Declarative Aspects of Multicore Programming},
  OPTpages =     {},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  month =        jan,
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote =         {To appear},
  OPTannote =    {},
  OPTurl = ""
}


@InProceedings{ec2,
  author =       {Zappa Nardelli,  Francesco  and Peter Sewell and Jaroslav \v{S}ev\v{c}\'{\i}k and Susmit
  Sarkar and Scott Owens and Luc Maranget and Mark Batty and Jade Alglave},
  title =        {Relaxed memory models must be rigorous},
  OPTcrossref =  {},
  OPTkey =       {},
  booktitle =    {Proceedings of Exploiting Concurrency Efficiently and Correctly -- (EC)2.  CAV 2009 Workshop. Grenoble, France},
  pages =        {4pp},
  year =         {2009},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  month =        jun,
  OPTorganization = {},
  OPTpublisher = {},
  note =         {\url{http://www.cs.utah.edu/ec2/}},
  OPTannote =    {}
}


@inproceedings{tphols09,
  author    = {Scott Owens and Susmit Sarkar and Peter Sewell},
  title     = {A better x86 memory model: {x86-TSO}},
  booktitle = {TPHOLs 2009: Theorem Proving in Higher Order Logics, LNCS 5674},
  pages     ={391--407},
  year      = {2009},
}


@Article{cacm,
  author =       {Peter Sewell and Susmit Sarkar and Scott Owens and Zappa Nardelli, Francesco  and Magnus O. Myreen},
  title =        {{x86-TSO}: A Rigorous and Usable Programmer's Model for x86 Multiprocessors},
  journal =      {Communications of the ACM},
  year =         {2010},
  OPTkey =       {},
  volume =       {53},
  number =       {7},
  pages =        {89--97},
  month =        jul,
  note =         {(Research Highlights)},
  OPTannote =    {}
}


@InProceedings{npict-r2d2,
  author =       {Peter Sewell and Pawe{\l} Wojciechowski},
  title =        {Verifying Overlay Networks for Relocatable Computations
(or: {Nomadic Pict}, relocated)},
  OPTcrossref =  {},
  OPTkey =       {},
  booktitle =    {Proceedings of the workshop on The Rise and Rise of the Declarative Datacentre, Microsoft Research Technical Report MSR-TR-2008-61},
  pages =        {43--46},
  year =         {2008},
  OPTeditor =    {Karthikeyan Bhargavan, Andrew Gordon, Tim Harris, and Peter Toft},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  month =        may,
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote =      {},
  OPTannote =    {}
}

@Article{npict-toplas,
  author =       {Peter Sewell and Pawe{\l} Wojciechowski and Asis Unyapoth},
  title =        {Nomadic {Pict}: Programming Languages, Communication Infrastructure Overlays, and Semantics for Mobile Computation},
  journal =      {ACM Transactions on Programming Languages and Systems (TOPLAS)},
  year =         {2010},
  OPTkey =       {},
  volume =       {32},
  number =       {4},
  pages =        {1--63 (and electronic appendix, 33pp)},
  OPTmonth =     {},
  OPTnote =         {(Accepted for publication, 3 Sep.~2009)},
  OPTannote =    {}
}


@InProceedings{mtv09,
  author =       {Peter Sewell},
  title =        {Multiprocessor Architectures Don't Really Exist (But They Should)},
  OPTcrossref =  {},
  OPTkey =       {},
  booktitle =    {Proc.~10th International Workshop on Microprocessor Test and Verification (MTV), Austin, Texas},
  pages =        {2},
  year =         {2009},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  OPTmonth =     {},
  OPTorganization = {},
  OPTpublisher = {},
  note =         {Invited session on Verification issues for multi-core systems},
  OPTannote =    {}
}

@inproceedings{cav2010,
  author    = {Jade Alglave and
               Luc Maranget and
               Susmit Sarkar and
               Peter Sewell},
  title     = {Fences in Weak Memory Models},
  booktitle = {Proc.~CAV: 22nd International Conference on Computer Aided Verification, LNCS 6174},
  year      = {2010},
  pages     = {258-272},
  ee        = {http://dx.doi.org/10.1007/978-3-642-14295-6_25},
  OPTcrossref  = {DBLP:conf/cav/2010},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/cav/2010,
  editor    = {Tayssir Touili and
               Byron Cook and
               Paul Jackson},
  title     = {Computer Aided Verification, 22nd International Conference,
               CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings},
  booktitle = {CAV},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6174},
  year      = {2010},
  isbn      = {978-3-642-14294-9},
  ee        = {http://dx.doi.org/10.1007/978-3-642-14295-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@InProceedings{cpp-popl,
  OPTauthor =       {M. Batty and S. Owens and S. Sarkar and P. Sewell and T. Weber},
  author =       {Mark Batty and Scott Owens and Susmit Sarkar and Peter Sewell and Tjark Weber},
  title =        {Mathematizing {C++} Concurrency},
  OPTcrossref =  {},
  OPTkey =       {},
  booktitle =    {Proc.~POPL},
  OPTpages =     {},
  year =         {2011},
  OPTeditor =       {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  OPTmonth =     {},
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote =      {},
  OPTannote =    {}
}


@InProceedings{compcertTSO-popl,
  author =       {Jaroslav \v{S}ev\v{c}\'{\i}k and Viktor Vafeiadis and Zappa Nardelli, Francesco  and Suresh Jagannathan and Peter Sewell},
  title =        {Relaxed-Memory Concurrency and Verified Compilation},
  OPTcrossref =  {},
  OPTkey =       {},
  booktitle =    {Proc.~POPL},
  OPTpages =     {},
  year =         {2011},
  OPTeditor =       {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  OPTmonth =     {},
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote =      {},
  OPTannote =    {}
}

@inproceedings{Alglave:2011:LRT:1987389.1987395,
 author = {Alglave, Jade and Maranget, Luc and Sarkar, Susmit and Sewell, Peter},
 title = {Litmus: running tests against hardware},
 booktitle = {Proceedings of the 17th international conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS): part of the joint European conferences on Theory and Practice of Software (ETAPS)},
 series = {TACAS'11/ETAPS'11},
 year = {2011},
 isbn = {978-3-642-19834-2},
 location = {Saarbr\&\#252;cken, Germany},
 pages = {41--44},
 numpages = {4},
 url = {http://dl.acm.org/citation.cfm?id=1987389.1987395},
 acmid = {1987395},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
} 


@inproceedings{Sewell:2010:MEA:1806651.1806660,
 author = {Sewell, Peter},
 title = {Memory, an elusive abstraction},
 booktitle = {Proc.~ISMM: the International Symposium on Memory Management},
 OPTseries = {ISMM '10},
 year = {2010},
 isbn = {978-1-4503-0054-4},
 location = {Toronto, Ontario, Canada},
 pages = {51--52},
 numpages = {2},
 url = {http://doi.acm.org/10.1145/1806651.1806660},
 doi = {http://doi.acm.org/10.1145/1806651.1806660},
 acmid = {1806660},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {relaxed memory models, semantics},
}


@InProceedings{pldi105,
  author =       {Susmit Sarkar and Peter Sewell and Jade Alglave and Luc Maranget and Derek Williams},
  title =        {Understanding {POWER} Multiprocessors},
  OPTcrossref =  {},
  OPTkey =       {},
  booktitle =    {Proc.~PLDI},
  OPTpages =     {},
  year =         {2011},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  OPTmonth =     {},
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote =      {},
  OPTannote =    {}
}


@inproceedings{Gordon:2011:RMV:1926385.1926439,
 author = {Gordon, Andrew D. and Harper, Robert and Harrison, John and Jeffrey, Alan and Sewell, Peter},
 title = {{Robin Milner} 1934--2010: verification, languages, and concurrency},
 booktitle = {Proceedings of POPL: the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
 OPTseries = {POPL '11},
 year = {2011},
 isbn = {978-1-4503-0490-0},
 OPTlocation = {Austin, Texas, USA},
 pages = {473--474},
 numpages = {2},
 url = {http://doi.acm.org/10.1145/1926385.1926439},
 doi = {http://doi.acm.org/10.1145/1926385.1926439},
 OPTacmid = {1926439},
 OPTpublisher = {ACM},
 OPTaddress = {New York, NY, USA},
 OPTkeywords = {Robin Milner},
} 

@InProceedings{popl2012,
  author =       {Mark Batty and Kayvan Memarian and Scott Owens and Susmit Sarkar and Peter Sewell},
  title =        {{Clarifying and Compiling C/C++ Concurrency: from C++11 to POWER}},
  OPTcrossref =  {},
  OPTkey =       {},
  booktitle =    {Proceedings of POPL 2012: The 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Philadelphia)},
  OPTpages =     {},
  year =         {2012},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  OPTmonth =     {},
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote =         {12 pp},
  OPTannote =    {}
}


@InProceedings{pldi2012,
  author = 	 {Susmit Sarkar and Kayvan Memarian and Scott Owens and Mark Batty and Peter Sewell and Luc Maranget and Jade Alglave and Derek Williams},
  title = 	 {Synchronising {C/C++} and {POWER}},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle =	 {Proceedings of {PLDI}, the 33rd {ACM SIGPLAN conference on Programming Language Design and Implementation (Beijing)}},
  OPTpages = 	 {},
  year =	 {2012},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}
@inproceedings{DBLP:conf/cav/Mador-HaimMSMAOAMSW12,
  author    = {Sela Mador-Haim and
               Luc Maranget and
               Susmit Sarkar and
               Kayvan Memarian and
               Jade Alglave and
               Scott Owens and
               Rajeev Alur and
               Milo M. K. Martin and
               Peter Sewell and
               Derek Williams},
  title     = {An Axiomatic Memory Model for {POWER} Multiprocessors},
  booktitle = {Proc.~CAV},
  year      = {2012},
  pages     = {495-512},
  ee        = {http://dx.doi.org/10.1007/978-3-642-31424-7_36},
  OPTcrossref  = {DBLP:conf/cav/2012},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}