Proof Appendix for Security Reasoning via Substructural Dependency Tracking

We claim in the paper that we have a proof of safety for the type system provided therein. We also reference, but do not discuss, an extended proof of non-interference from prior work. The paper proofs in this artifact substantiate these claims. Definitions excluded from the paper are given in Appendix D starting on page 32. Lemmas and theorems are given in Appendix E starting on page 37. The statement of the Fundamental Theorem is given starting on page 57. The safety corollary on which the paper concludes is given on page 63. The proof of non-interference is given starting on page 64, with the constant function theorem concluding on page 84.