Peter Sewell

Projects, Papers, and Software

The Semantics of Multiprocessor Machine Code: x86, Power, and ARM

• A Better x86 Memory Model: x86-TSO (Extended Version). Technical Report UCAM-CL-TR-745. Scott Owens, Susmit Sarkar, and Peter Sewell.
• A Better x86 Memory Model: x86-TSO . In TPHOLs 2009. Scott Owens, Susmit Sarkar, and Peter Sewell.
• The Semantics of x86-CC Multiprocessor Machine Code (in POPL 2009)
• The Semantics of Power and ARM Multiprocessor Machine Code (in DAMP 2009)

Ott: Tool Support for Semantics

• Ott: Effective Tool Support for the Working Semanticist (pdf) and (ps). Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, Rok Strniša. Draft full paper.
• Ott: Effective Tool Support for the Working Semanticist (pdf) and (ps). Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, Rok Strniša. In ICFP 2007.

The POPLmark Challenge

• Mechanized Metatheory for the Masses: The POPLmark Challenge Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. In TPHOLs 2005. Also in ps.
• It is Time to Mechanize Programming Language Metatheory Benjamin C. Pierce, Peter Sewell, Stephanie Weirich, and Steve Zdancewic. In Verified Software: Theories, Tools, Experiments, 2005.

Semantics for Network Protocols

• A rigorous approach to networking: TCP, from implementation to protocol to service . Tom Ridge, Michael Norrish, Peter Sewell. Also in pdf. In FM'08.
• Rigorous Protocol Design in Practice: An Optical Packet-Switch MAC in HOL . Adam Biltcliffe, Michael Dales, Sam Jansen, Tom Ridge, Peter Sewell. Also in pdf. In ICNP 2006. The protocol specification: SWIFT MAC Protocol: HOL Specification.
• Engineering with Logic: HOL Specification and Symbolic-Evaluation Testing for TCP Implementations . Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough. 14pp. Also in pdf. In POPL 2006.
• Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and Sockets. Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough. 12pp. Also in pdf. In SIGCOMM 2005.
• TCP, UDP, and Sockets: rigorous and experimentally-validated behavioural specification. Volume 1: Overview. Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough. 88pp. Technical Report 624. March 2005. Also in pdf.
• TCP, UDP, and Sockets: rigorous and experimentally-validated behavioural specification. Volume 2: The Specification. Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough. 386pp. Technical Report 625. March 2005. Also in pdf (with internal hyperlinks) and in ps 2up (good for printing).
• The TCP Specification: A Quick Introduction. 5pp. February 2005. Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough. Also in pdf.
• An approximation to the real TCP state diagram. This is a poster with a version of the `TCP state diagram' extracted from the specification. It is rather more complete than the usual diagram, but is still a very abstract and simplified view of the state space of our specification. It is intended to be printed at A1 size or bigger. Also in pdf.
• Rigour is good for you and feasible: reflections on formal treatments of C and UDP sockets. Michael Norrish, Peter Sewell, Keith Wansbrough. In SIGOPS EW 2002. Also in ps.gz.
• Timing UDP: mechanized semantics for sockets, threads and failures. Keith Wansbrough, Michael Norrish, Peter Sewell, Andrei Serjantov. In ESOP 2002. Also in ps.gz and pdf.
• The UDP Calculus: Rigorous Semantics for Real Networking. Technical report 515. Andrei Serjantov, Peter Sewell, and Keith Wansbrough. Also in ps.gz.
• The UDP Calculus: Rigorous Semantics for Real Networking. Andrei Serjantov, Peter Sewell, and Keith Wansbrough. In TACS 2001. Also in ps.gz.

Language Design: Modules, Versioning, Marshalling, Update (more details on the Acute and HashCaml pages)

• Dynamic Rebinding for Marshalling and Update, via Redex-time and Destruct-time Reduction. Sewell, Stoyle, Hicks, Bierman, and Wansbrough. Journal of Functional Programming 18(4): 437-502, 2008. (c) CUP.
• The Java Module System: core design and semantic definition. Rok Strniša, Peter Sewell, Matthew Parkinson. In OOPSLA '07. LJAM web page.
• Type-Safe Distributed Programming for OCaml John Billings, Peter Sewell, Mark Shinwell, Rok Strniša. Also in pdf. In ML'06.
• Acute: high-level programming language design for distributed computation Peter Sewell, James J. Leifer, Keith Wansbrough, Francesco Zappa Nardelli, Mair Allen-Williams, Pierre Habouzit, Viktor Vafeiadis. Also in pdf. Journal of Functional Programming 17(4-5):547-612, 2007. (c) CUP.
• Here is a source release of the Acute system.
• Acute: high-level programming language design for distributed computation Peter Sewell, James J. Leifer, Keith Wansbrough, Francesco Zappa Nardelli, Mair Allen-Williams, Pierre Habouzit, Viktor Vafeiadis. In ICFP 2005. Also in pdf.
• Acute: high-level programming language design for distributed computation. Design rationale and language definition. Peter Sewell, James J. Leifer, Keith Wansbrough, Mair Allen-Williams, Francesco Zappa Nardelli, Pierre Habouzit, Viktor Vafeiadis. Technical report 605. Also in ps.
• Mutatis Mutandis: Safe and predictable dynamic software updating. Gareth Stoyle, Michael Hicks, Gavin Bierman, Peter Sewell, Iulian Neamtiu. ACM TOPLAS 29(4), 2007.
• Mutatis Mutandis: Safe and Predictable Dynamic Software Updating, with Gareth Stoyle, Mike Hicks, Gavin Bierman, and Iulian Naemtiu. In POPL 2005
• Global abstraction-safe marshalling with hash types James Leifer, Gilles Peskine, Peter Sewell, Keith Wansbrough. In ICFP 2003. Also in pdf.
• a Technical Report is also available, from here or here.
• Dynamic Rebinding for Marshalling and Update, with Destruct-time lambda Gavin Bierman, Michael Hicks, Peter Sewell, Gareth Stoyle, Keith Wansbrough. In ICFP 2003. Also in pdf.
• a Technical Report is also available, in pdf or ps.
• Formalising Dynamic Software Updating Gavin Bierman, Michael Hicks, Peter Sewell, Gareth Stoyle. In USE 2003. Also in pdf.
• Modules, Abstract Types, and Distributed Versioning. In POPL 2001. Also in pdf, dvi, and ps.gz.
• Modules, Abstract Types, and Distributed Versioning. Technical Report 506, Computer Laboratory, University of Cambridge. Also in pdf, dvi, and ps.gz. See also a few errata in the above.

Security

• Cassandra: Flexible Trust Management, Applied to Electronic Health Records. Moritz Y. Becker and Peter Sewell. In CSFW04.
• For more details, including the complete example policy, see here and Moritz Becker's PhD thesis.
• Cassandra: Distributed Access Control Policies with Tunable Expressiveness. Moritz Y. Becker and Peter Sewell. In POLICY 2004.
• Passive Attack Analysis for Connection-Based Anonymity Systems. Andrei Serjantov and Peter Sewell. ESORICS 2003.
• Secure Composition of Untrusted Code: Box pi, Wrappers, and Causality Types. Peter Sewell and Jan Vitek. In Journal of Computer Security.
• Secure Composition of Untrusted Code: Wrappers and Causality Types. Peter Sewell and Jan Vitek. In the Computer Security Foundations Workshop, CSFW-13, July 2000.
• Secure Composition of Untrusted Code: Wrappers and Causality Types. Peter Sewell and Jan Vitek. Technical Report 478, Computer Laboratory, University of Cambridge, November 1999.
• Secure Composition of Insecure Components. Peter Sewell and Jan Vitek. In the Computer Security Foundations Workshop, CSFW-12, June 1999.
• Secure Composition of Insecure Components. Peter Sewell and Jan Vitek. Technical Report 463, Computer Laboratory, University of Cambridge, April 1999.

Language and Communication Infrastructure for Mobile Computing (more details on the Nomadic Pict page)

• Nomadic Pict: Programming Languages, Communication Infrastructure Overlays, and Semantics for Mobile Computation. Sewell, Wojciechowski, and Unyapoth. In TOPLAS 2010 32(4).
• Verifying Overlay Networks for Relocatable Computations (or: Nomadic Pict, relocated). Sewell and Wojciechowski. Position paper for the MSR/HP Labs research meeting on The Rise and Rise of the Declarative Datacentre, May 2008.
• Nomadic Pict: Correct Communication Infrastructure for Mobile Computation. Asis Unypoth and Peter Sewell. In POPL 2001. Also in pdf, dvi, and ps.gz.
• Nomadic Pict: Language and Infrastructure Design for Mobile Agents, Pawel Wojciechowski and Peter Sewell. In ASA/MA'99 (First International Symposium on Agent Systems and Applications/Third International Symposium on Mobile Agents), October 1999. An extended version appeared in IEEE Concurrency vol 8 no 2, 2000.
• Location-Independent Communication for Mobile Agents: a Two-Level Architecture. Peter Sewell, Pawel Wojciechowski, Benjamin Pierce. Technical Report 462, Computer Laboratory, University of Cambridge, April 1999. A version of this appeared in Internet Programming Languages, LNCS 1686.
• Location Independence for Mobile Agents. Peter Sewell, Pawel Wojciechowski, Benjamin Pierce. In the Workshop on Internet Programming Languages, 1998. Largely superseded by the technical report above.

XML scripting

• Iota: A concurrent XML scripting language with applications to Home Area Networking. G.M. Bierman and P. Sewell. Technical report 557, Computer Laboratory, University of Cambridge.

Models for Name-Passing

• Models for Name-Passing Processes: Interleaving and Causal.Gian Luca Cattani and Peter Sewell. Technical report 505, Computer Laboratory, University of Cambridge. Also in pdf, dvi, and ps.gz. Revised version to appear in Information and Computation
• Models for Name-Passing Processes: Interleaving and Causal (Extended Abstract). Gian Luca Cattani and Peter Sewell. In LICS 2000.

Applied Pi Tutorial

• Applied Pi - A Brief Tutorial. Technical Report 498, Computer Laboratory, University of Cambridge 2000. They are an extended version of a chapter Pi Calculi in Formal Methods for Distributed Programming, edited by H. Bowman and J. Derrick, CUP. Also in pdf.
• A Brief Introduction to Applied Pi. Notes from my lectures at the MATHFIT meeting on Recent Advances in Semantics and Types for Concurrency: Theory & Practice, Imperial College, July, 1998. The slides and other pointers are here.

Operational Semantics

• From Rewrite Rules to Bisimulation Congruences. A preprint of a paper in a special issue of Theoretical Computer Science for CONCUR 98. This supersedes the following.
• From Rewrite Rules to Bisimulation Congruences. Technical Report 444, Computer Laboratory, University of Cambridge, June 1998. Here is the abstract and short and long versions, and the same in cmr: short and long. An extended abstract of this appeared in CONCUR 98, LNCS 1466.

Locality Typing

• Global/Local Subtyping and Capability Inference for a Distributed pi-calculus . An extended abstract of this appeared in ICALP 98, LNCS 1443.
• Global/Local Subtyping for a Distributed pi-calculus . Technical Report 435, Computer Laboratory, University of Cambridge, August 1997. Here is the abstract and a cmr version

Observational Semantics for Concurrent Languages

• On Implementations and Semantics of a Concurrent Programming Language . This appeared in the proceedings of CONCUR 97, LNCS 1243. Here is the abstract and a cmr version

Hardware Modelling

• Design Rules and Abstraction (from branching and real time) (a draft). A short version of this appeared in the proceedings of the 3rd Workshop on Designing Correct Circuits, September 1996. Here is the abstract.

Process Algebra

• Nonaxiomatisability of equivalences over finite state processes. In Annals of Pure and Applied Logic. This supersedes the following paper and part of my thesis. Here is the abstract; please contact me for a preprint.
• Bisimulation is not Finitely (first order) Equationally Axiomatisable. This appeared in LICS '94. Here is the abstract.
• The Algebra of Finite State Processes. This is my PhD thesis. Here is the abstract and a cmr version.

Copyright

(c) 1994,1999,2000 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

The published versions of the ESOP 2002, TACS 2001, CONCUR 97, ICALP 98, CONCUR 98 and IPL papers are (c) Springer-Verlag; the versions above may differ from these.

The published version of the TCS rewrite rules paper is (c) Elsevier Science B.V.