Appendix to CMod: Modular Information Hiding and Type-Safe Linking for C

Abstract

This brief note is an appendix to the paper "CMod: Modular Information Hiding and Type-Safe Linking for C." It consists of the proof of soundness for the formal language presented in that paper.