Related work and bibliography
This page links to background and sources.
Pointer and object model
Robbert Krebbers’s model of C (Krebbers 2015, PhD thesis).
The formal model of pointer provenance for C given by Cerberus (POPL’19).
A Provenance-aware Memory Object Model for C. Working paper N2577 of the C standards committee (ISO TC1/SC22/WG14), September 30, 2020
Work by Ramananandro et al. (e.g. POPL’12).
LLVM’s twin semantics “Reconciling high-level optimizations and low-level code in LLVM”, OOPSLA’18