Peter Sewell
Reader in Computer Science and EPSRC Leadership Fellow,
Computer
Laboratory,
University of Cambridge.
Fellow of
Wolfson college.
Here are my contact details,
and a
photo
Post-doc Positions
We are looking for a Post-Doctoral Research Associate and a Senior
Research Associate to join a lively
group working on the semantics of real-world computer systems. Here are the
adverts:
RA, SRA;
the closing date is 4 May 2012.
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 are all my papers and software
and my bibtex data, and the Cambridge
Programming, Logic,
and Semantics Group.
- Synchronising
C/C++ and POWER. Susmit
Sarkar, Kayvan Memarian, Scott Owens, Mark Batty, Peter Sewell, Luc
Maranget, Jade Alglave, Derek Williams.
In PLDI 2012.
- 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.
- Understanding POWER Multiprocessors. Susmit
Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, Derek Williams. In
PLDI 2011
- Relaxed-Memory Concurrency
and Verified Compilation. Jaroslav Sevcik, Viktor Vafeiadis,
Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell.
In POPL 2011
- Mathematizing C++
Concurrency.
Mark Batty,
Scott Owens,
Susmit Sarkar,
Peter Sewell, and
Tjark Weber.
In POPL 2011
- Litmus: Running Tests Against Hardware.
Jade Alglave, Luc Maranget, Susmit Sarkar and Peter Sewell.
Tool Demonstration Paper.
In TACAS 2011.
- 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.
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
-
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.
-
Nomadic Pict: Programming Languages, Communication Infrastructure Overlays, and
Semantics for Mobile Computation. Sewell, Wojciechowski, and
Unyapoth. In TOPLAS 2010 32(4).
-
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
Mair Allen-Williams
Gavin Bierman
Adam Biltcliffe
Steve Bishop
Gian Luca Cattani
Michael Dales
Matthew Fairbairn
Pierre Habouzit
Michael Hicks
Sam Jansen
James Leifer
Michael Norrish
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.]
