Peter Sewell
Previous Projects, Papers, and Software
-
Fences in Weak Memory Models (Extended Version).
Jade Alglave, Luc Maranget, Susmit Sarkar and Peter Sewell
In FMSD, Volume 40, Number 2, April 2012.
-
Fences in Weak Memory Models.
Jade Alglave, Luc Maranget, Susmit Sarkar and Peter Sewell
In CAV 2010.
-
Ott: Effective Tool Support for the Working Semanticist (pdf).
Peter Sewell,
Francesco Zappa Nardelli,
Scott Owens,
Gilles Peskine,
Thomas Ridge,
Susmit Sarkar,
Rok Strniša. Journal of Functional Programming 20(1):71-122, 2010
-
Nomadic Pict: Programming Languages, Communication Infrastructure Overlays, and
Semantics for Mobile Computation. Sewell, Wojciechowski, and
Unyapoth. In TOPLAS 2010 32(4).
-
A Better x86 Memory Model: x86-TSO
. In TPHOLs 2009. Scott Owens, Susmit
Sarkar, and Peter Sewell.
-
A Better x86 Memory Model: x86-TSO
(Extended Version). Technical Report UCAM-CL-TR-745. Scott Owens, Susmit
Sarkar, and Peter Sewell.
-
Relaxed memory models must be
rigorous. In EC^2.
Francesco Zappa Nardelli, Peter Sewell, Jaroslav Sevcik, Susmit
Sarkar, Scott Owens, Luc Maranget, Mark Batty, and Jade Alglave
- The Semantics of x86-CC Multiprocessor
Machine Code
(in POPL 2009).
Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli, Scott Owens,
Tom Ridge, Thomas Braibant, Magnus O. Myreen, and Jade Alglave.
- The Semantics of Power and ARM Multiprocessor
Machine Code
(in DAMP
2009).
Jade Alglave, Anthony Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit
Sarkar, Peter Sewell, and Francesco Zappa Nardelli. Note that the
model presented here has some major flaws; further work is in
progress.
-
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.
-
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 Java Module System: core design and semantic definition.
Rok Strniša,
Peter Sewell,
Matthew Parkinson.
In
OOPSLA '07.
LJAM web page.
-
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.
-
Mutatis Mutandis: Safe and predictable dynamic software
updating. Gareth Stoyle, Michael Hicks, Gavin Bierman, Peter
Sewell, Iulian Neamtiu. ACM TOPLAS 29(4), 2007.
-
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.
-
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
Models for Name-Passing
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
Observational Semantics for Concurrent Languages
Hardware Modelling
Process Algebra
Some of the fonts used in the older papers are not supported at all sites - if
there are printing difficulties, try the cmr versions.
[Validate this page.]