Vadim Zaliva, Kayvan Memarian, Ricardo Almeida, Jessica Clarke, Brooks Davis, Alex Richardson, David Chisnall, Brian Campbell, Ian Stark, Robert N. M. Watson, and Peter Sewell. ACM ASPLOS 2024, 2024.
Gives a mechanised semantics for CHERI C covering capabilities, pointer provenance, and undefined behaviour.