Towards formally verified compilation of tag-based policy enforcement. - Chris Chhak; Andrew Tolmach; Sean Noble Anderson (CPP, 2021)

Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model. - Andrew Tolmach; Chris Chhak; Sean Noble Anderson (ITP, 2024)