LMS/BCS-FACS Evening Seminars

In association with the British Computer Society Formal Aspects of Computing Science (BCS-FACS), the LMS hosts an annual evening seminar on aspects of the computer science–mathematics interface. These events are free to anyone who wishes to attend, and have attracted high-quality speakers.

LMS/BCS-FACS Evening Seminar 2021

This event was held on 18th November 2021. You can watch a video of the talk here.

Speaker: Professor Peter Sewell (University of Cambridge) 
Title: Underpinning mainstream engineering with mathematical semantics
Date: Thursday 18th November 2021
Venue: De Morgan House, London, and online

Email Katherine Wright, Society & Research Officer, if you have any questions: lmscomputerscience@lms.ac.uk.


Despite 80+ years of research on semantics and verification, mainstream computer systems and their engineering development processes remain almost entirely non-formal, reliant on ad hoc testing and prose specifications.  These have been good enough for industry to thrive, but their inability to exclude errors is one of the root causes of today's endemic security failures.

In this talk I'll discuss what it takes to put mathematically rigorous semantics to work for full-scale mainstream systems, touching on scientific, engineering, and social aspects, and on the benefits and costs.  This will draw on work with many colleagues on various key interfaces: processor architectures, programming languages, and network protocols; and on the CHERI and Morello projects, extending conventional architectures and languages with hardware support for capabilities, for fine-grained memory protection and encapsulation.

Taking mainstream engineering artifacts seriously also prompts new theory and tools, e.g. for the relaxed shared-memory concurrency semantics of real machines, quite different from traditional concurrency semantics, and for the semantics of C and of CHERI capabilities.


Peter Sewell is a Professor of Computer Science at the University of Cambridge.  His research aims to enable rigorous semantics-based engineering of mainstream systems, including real-world concurrency semantics, instruction-set semantics, and CHERI.  His PhD was with Robin Milner in Edinburgh.  He has held ERC AdG, EPSRC, and Royal Society research fellowships. With Watson, Moore, and Arm, he was one of the instigators of the UKRI Digital Security by Design programme, supporting development of the Arm Morello prototype CHERI Armv8-A architecture, processor, software, and semantics.

Previous Seminars:


Professor Marta Kwiatkowska - When to trust a self-driving car


Professor Bill Roscoe - Verifying CSP and its offspring


Professor Erika Ábrahám - Symbolic Computation Techniques in SMT Solving


Professor Muffy Calder - Probabilistic Formal Analysis of Software Usage Styles in the Wild


Professor Roland Backhouse - The Mathematics of Programme Construction


Professor Joel Ouaknine - Decision Problems for Linear Recurrecnce Sequences


Professor Philippa Gardner - Views: Compositional Reasoning for Computer Programs


Professor Jack Copeland - The Mathematical Objection: Turing, Gödel and Penrose on the Mind


Professor Andrew Ireland - Reasoned Modelling: Towards Decision Support for System Designers.


Professor Peter O’Hearn - Reasoning about Programmes Using a Scientific Method


Professor Mike Gordon, FRS - Forward with Hoare.


Professor John Tucker - The Equations of Computer Science