Peter Sewell
Professor of Computer Science and EPSRC Leadership Fellow,
Computer
Laboratory,
University of Cambridge.
Fellow of
Wolfson college.
Member of the Cambridge
Programming, Logic,
and Semantics Group.
Here are my contact details,
and a
photo
Researcher and Research Engineer Positions in Rigorous Engineering
for Mainstream Systems (REMS)
Applications are invited for several postdoctoral researcher and postgraduate
research engineer positions: see REMS for details.
PhD CASE Studentship on ARM architectural semantics
Applications are invited for a fully funded PhD CASE studentship at
the University of Cambridge Computer Laboratory, with industrial
sponsorship from ARM Ltd; here are more details.
Teaching
Research
My research aims to put the engineering of real-world computer
systems on solid foundations, developing techniques -both
mathematically rigorous and pragmatically useful-
to enable the
construction of systems that are better-understood, more robust, and
more secure.
To do this requires tightly integrated theoretical and practical
research, spanning a range of Computer Science.
This is, broadly, applied semantics: I work in
programming languages, networking, and security,
developing and using techniques from
semantics, type systems, automated reasoning, and concurrency theory.
Research Topics
Here is my bibtex data.
Engineering with Logic: Rigorous Specification and Validation for TCP/IP and the Sockets API.
Steve Bishop, Matthew Fairbairn, Michael Norrish, Tom Ridge, Peter Sewell, Michael Smith, Keith Wansbrough. Draft.
- A Tutorial
Introduction to the ARM and POWER Relaxed Memory Models. Luc
Maranget, Susmit Sarkar, and Peter Sewell. Draft.
- CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency. Jaroslav Sevcik, Viktor Vafeiadis,
Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell.
To appear in J.ACM.
(more details)
-
An Axiomatic Memory Model for POWER Multiprocessors.
Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo M. K. Martin, Peter Sewell, Derek Williams.
In CAV 2012.
(more details)
- Synchronising
C/C++ and POWER. Susmit
Sarkar, Kayvan Memarian, Scott Owens, Mark Batty, Peter Sewell, Luc
Maranget, Jade Alglave, Derek Williams.
In PLDI 2012.
(more details)
- Clarifying and Compiling C/C++ Concurrency: from C++11 to POWER.
Mark Batty,
Kayvan Memarian,
Scott Owens,
Susmit Sarkar, and
Peter Sewell. In POPL 2012.
(more details)
- Understanding POWER Multiprocessors. Susmit
Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, Derek Williams. In
PLDI 2011
(more details)
- Litmus: Running Tests Against Hardware.
Jade Alglave, Luc Maranget, Susmit Sarkar and Peter Sewell.
Tool Demonstration Paper.
In TACAS 2011.
- Relaxed-Memory Concurrency
and Verified Compilation. Jaroslav Sevcik, Viktor Vafeiadis,
Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell.
In POPL 2011
(more details)
- Mathematizing C++
Concurrency.
Mark Batty,
Scott Owens,
Susmit Sarkar,
Peter Sewell, and
Tjark Weber.
In POPL 2011
(more details)
- x86-TSO: A Rigorous and Usable Programmer's Model
for x86 Multiprocessors.
Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli,
Magnus O. Myreen.
In Communications
of the ACM (Research Highlights) 2010 No.7.
-
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.
I maintain
a page of
Action
Calculi links.
People
Some Coauthors
Jade Alglave
Mair Allen-Williams
Peter Boehm
Gavin Bierman
Adam Biltcliffe
Steve Bishop
Gian Luca Cattani
Michael Dales
Mike Dodds
Matthew Fairbairn
Pierre Habouzit
Michael Hicks
Sam Jansen
James
Leifer
Sela Mador-Haim
Luc Maranget
Michael Norrish
Scott Owens
Gilles Peskine
Benjamin Pierce
Tom Ridge
Susmit Sarkar
Jaroslav Sevcik
Mark Shinwell
Michael Smith
Viktor Vafeiadis
Jan Vitek
Keith Wansbrough
Stephanie Weirich
Francesco Zappa Nardelli
Steve Zdancewic
Current RAs
PhD Students
Other
Linepithema humile
A few things
Another photo
[Validate this page.]
