Peter Sewell

Professor of Computer Science and EPSRC Leadership Fellow, Computer Laboratory, University of Cambridge
Member of the Cambridge Programming, Logic, and Semantics Group
Fellow of Wolfson college

Here are my contact details, a photo, short bio, and CV

Jobs

We expect to recruit several more postdoctoral researcher and postgraduate research engineer positions for the REMS project over the next few years.

Teaching

Research

My research aims to put the engineering of real-world computer systems on better foundations, developing techniques (both mathematically rigorous and pragmatically useful) to make systems that are better-understood, more robust, and more secure. This applied semantics needs tightly integrated theoretical and practical research, spanning a range of Computer Science: I work in architectural description, programming languages, networking, and security, developing and using techniques from semantics, type systems, automated reasoning, and concurrency theory.

Research Projects

REMS: Rigorous Engineering for Mainstream Systems

Research Topics

I also maintain a page of Action Calculi links.

Recent Papers (with Previous Papers and bibtex data)

Lem: reusable engineering of real-world semantics. Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, and Peter Sewell. In ICFP 2014.
POPL 2014 PC Chair Report. Peter Sewell. In ACM SIGPLAN Notices.
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. 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.

Funding

REMS: Rigorous Engineering for Mainstream Systems. EPSRC Programme Grant EP/K008528/1, 2013-2019.
Semantic Foundations for Real-World Systems. EPSRC Leadership Fellowship EP/H005633/1. 2009-2014.
ARM Architectural Semantics EPSRC/ARM Industrial CASE PhD studentship, 2014
...previous funding

Meetings

ITP 2014: Conference on Interactive Theorem Proving (invited speaker)
CHLLP 2014: Workshop on Certification of high-level and low-level programs (in the Institut Henri Poincare thematic trimester on Semantics of proofs and certified mathematics, 2014 (invited speaker)
PLMW 2014: SIGPLAN Programming Languages Mentoring Workshop (invited speaker)
POPL 2014 (PC chair)
PiP 2014: first workshop on Principles in Practice, co-located with POPL 2014 (co-chair)
CPP: the 3rd international conference on Certified Programs and Proofs, 2013 (PC)
SLS 2013: Microsoft Research Workshop on Scalable Language Specification, (invited speaker)
VCP 2013: Microsoft Research Workshop on Verified Concurrent Programmes: Theory, Tools and Experiments, (invited speaker)
Linux Collaboration Summit, 2013 (invited speaker)
SRC/NSF/CCC Workshop on Convergence of Software Assurance Methodologies and Trustworthy Semiconductor Design and Manufacture (SA+TS), 2013 (invited speaker)
PLMW 2013: SIGPLAN Programming Languages Mentoring Workshop (invited speaker)
POPL 2013 (PC)
ICFP 2012 (invited speaker)
CONCUR 2012 (invited speaker)
Microsoft Cambridge PhD School 2012, TRANSFORM (invited speaker)
Milner Symposium, 2012 (invited speaker)
...previous meetings

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 Thomas Tuerk Viktor Vafeiadis Jan Vitek Keith Wansbrough Stephanie Weirich Francesco Zappa Nardelli Steve Zdancewic

Current RAs

PhD Students

Christopher Pulte 2014-.
Jean Pichon 2013-.
Shaked Flur 2013-.
Kyndylan Nienhuis 2013-.
Justus Matthiesen 2012-.
Kayvan Memarian 2011-.
Mark Batty 2009-2014. The C11 and C++11 Concurrency Model
Rok Strniša 2005-2010. Formalising, improving, and reusing the Java Module System
John Billings 05-. Switched to work on Metarouting with Tim Griffin.
Gareth Stoyle 2001-2006. Dynamic Software Updating
Moritz Becker 2001-2005. Distributed trust management, applied to electronic health records.
Andrei Serjantov -2004. On the Anonymity of Anonymity Systems
Asis Unyapoth -2001. Nomadic Pi Calculi: Expressing and Verifying Infrastructure for Mobile Computation
Pawel Wojciechowski -2000. Nomadic Pict: Language and Infrastructure Design for Mobile Computation

Other

Linepithema humile

Some tangible things

Litmus Test shop

[Validate this page.]