mugshot

Peter Sewell

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

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

REMS group (gallery)   Students and Postdocs (list)   Meetings   Funding   Group papers (by date)   Group papers (by topic)   Software

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 architecture specification, programming languages, verification, security, and networking, developing and using techniques from semantics, type systems, automated reasoning, and concurrency theory.

REMS logo Our REMS group (Rigorous Engineering for Mainstream Systems) does this, in collaboration with Semantics, Systems, Security, and Computer Architecture colleagues in Cambridge, other academics worldwide, and colleagues in Arm, Google, IBM, and elsewhere. REMS was originally funded by the eponymous EPSRC REMS Programme Grant, with Imperial and Edinburgh; it now continues with other funding, including the EU ERC Advanced Grant ELVER: Engineering with Logic and Verification: Mathematically Rigorous Engineering for Safe and Secure Computer Systems, and donations from Arm and Google.

The CHERI project, led by Robert Watson, Simon Moore, and myself at Cambridge, and Peter Neumann at SRI International, extends conventional hardware Instruction-Set Architectures (ISAs) with new architectural features to enable fine-grained memory protection and highly scalable software compartmentalization. It is a hardware/software/semantics co-design project, involving architecture design, hardware implementation, system software adaption, and formal semantics and mechanised proof of security properties. The UKRI Digital Security by Design Challenge, with £70m government and £117m industry funding from 2019--2024, is developing the industrial prototype Arm Morello CHERI-ARM 64-bit CPU, SoC, and board, to evaluate and demonstrate the mass-market industrial feasibility of CHERI. Here are our DSbD pages.

Recent Papers

Research Topics

I also maintain a page of Action Calculi links.

Other

Another photo

[Validate this page.]