This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.

Peter Sewell

Peter Sewell, Cambridge: the ISA-semantics cluster this corpus leans on -- Sail and Isla, the rigorous ARMv8 and RISC-V models, relaxed memory. Six records, 2016-2026. NOT Thomas Sewell of klein2009sel4, a different person.

ArchSem: Reusable Rigorous Semantics of Relaxed Architectures

Thibaut Pérami and others (2026) · Proceedings of the ACM on Programming Languages

Escaping the Quicksand: A Call to Arms

Peter Sewell and others (2026)

Precise exceptions in relaxed architectures

Ben Simner and others (2025) · ACM

Isla: integrating full-scale ISA semantics and axiomatic concurrency models

Alasdair Armstrong and others (2024) · Formal Methods in System Design

Verified Security for the Morello Capability-enhanced Prototype Arm Architecture

Thomas Bauereiss and others (2022) · Programming Languages and Systems (ESOP 2022)

Relaxed virtual memory in Armv8-A

Ben Simner and others (2022) · Programming Languages and Systems · Springer International Publishing

Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models

Alasdair Armstrong and others (2021) · Springer International Publishing

Cornucopia: Temporal Safety for CHERI Heaps

Nathaniel Wesley Filardo and others (2020) · Proceedings - IEEE Symposium on Security and Privacy/Proceedings of the ... IEEE Symposium on Security and Privacy · IEEE Computer Society

N2577: A provenance-aware memory object model for C

Jens Gustedt and others (2020)

Rigorous Engineering for Hardware Security: Formal Modelling and Proof in the CHERI Design and Implementation Process

Kyndylan Nienhuis and others (2020) · 2020 IEEE Symposium on Security and Privacy (SP)

ARMv8-A System Semantics: Instruction Fetch in Relaxed Architectures

Ben Simner and others (2020) · Springer International Publishing

Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 8)

Robert N. M. Watson and others (2020) · CL Technical Reports

DSbD CHERI and Morello Capability Essential IP (Version 1)

Robert N. M. Watson and others (2020) · Computer Laboratory, University of Cambridge

ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS

Alasdair Armstrong and others (2019) · Proceedings of the ACM on Programming Languages · Association for Computing Machinery

CheriABI: Enforcing valid pointer provenance and minimizing pointer privilege in the POSIX C run-time environment

Brooks Davis and others (2019) · ASPLOS 2019: Proceedings of the 24th International Conference on Architectural Support for Programming Languages and Operating Systems

Exploring C semantics and pointer provenance

Kayvan Memarian and others (2019) · Proceedings of the ACM on Programming Languages · Association for Computing Machinery

Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 7)

Robert N. M. Watson and others (2019) · CL Technical Reports

Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8

Christopher Pulte and others (2018) · Proceedings of the ACM on Programming Languages · Association for Computing Machinery

Mixed-size concurrency: ARM, POWER, C/C++11, and SC

Shaked Flur and others (2017)

Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA

Shaked Flur and others (2016) · Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016)

A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions

Jean Pichon-Pharabod and others (2016) · ACM

The Problem of Programming Language Concurrency Semantics

Mark Batty and others (2015) · Programming Languages and Systems · Springer Berlin Heidelberg

An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors

Kathryn E. Gray and others (2015) · ACM

Lem: reusable engineering of real-world semantics

Dominic P. Mulligan and others (2014) · ACM SIGPLAN International Conference on Functional Programming (ICFP)

Clarifying and compiling C/C++ concurrency: from C++11 to POWER

Mark Batty and others (2012) · ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)

A tutorial introduction to the ARM and POWER relaxed memory models, October 2012

Luc Maranget and others (2012) · Draft. URL:

Synchronising C/C++ and POWER

Susmit Sarkar and others (2012) · ACM

Litmus: Running Tests against Hardware

Jade Alglave and others (2011) · Lecture notes in computer science · Springer Science+Business Media

Lem: A Lightweight Tool for Heavyweight Semantics

Scott Owens and others (2011) · Springer Berlin Heidelberg

Understanding POWER multiprocessors

Susmit Sarkar and others (2011) · ACM

Fences in Weak Memory Models

Jade Alglave and others (2010) · Lecture notes in computer science · Springer Science+Business Media

x86-TSO: A rigorous and usable programmer's model for x86 multiprocessors

Peter Sewell and others (2010) · Communications of the ACM · Association for Computing Machinery (ACM)

The semantics of power and ARM multiprocessor machine code

Jade Alglave and others (2009)

A Better x86 Memory Model: x86-TSO

Scott Owens and others (2009) · Springer Berlin Heidelberg

A better x86 memory model: x86-TSO (extended version)

Scott Owens and others (2009) · Computer Laboratory, University of Cambridge

The semantics of x86-CC multiprocessor machine code

Susmit Sarkar and others (2009) · ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)

Mechanized Metatheory for the Masses: The PoplMark Challenge

Brian E. Aydemir and others (2005) · Theorem Proving in Higher Order Logics · Springer Berlin Heidelberg