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

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

REMS logo This is in collaboration with many academic colleagues in Cambridge, Edinburgh, Aarhus, and elsewhere, and industry colleagues in Arm, Google, IBM, RISC-V International, and elsewhere. REMS (Rigorous Engineering for Mainstream Systems) was originally funded by the eponymous EPSRC REMS Programme Grant, with Imperial and Edinburgh; it continues with other funding, including the EU ERC AdG ELVER (2018-2024), the ERC/UKRI Frontier Guarantee AdG SAFER (2024-2029), and donations from Arm, Google, Intel, and Amazon.

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-2025, developed the industrial prototype Arm Morello CHERI-ARM 64-bit CPU, SoC, board, and software stack, to evaluate and demonstrate the mass-market industrial feasibility of CHERI. Here are our DSbD pages.

Recent REMS Group Papers

Blog articles

Talks

Research Topics

I also maintain a page of Action Calculi links.

Other

Another photo

[Validate this page.]