This supplement material contains the Isabelle/HOL theories relevant for readers of the Journal of Functional Programming Special Issue on Secure Compilation submission:
"Verified Secure Compilation for Mixed-Sensitivity Concurrent Programs" (R. Sison, T. Murray)

File: wr-compiler-jfp_c5e66ea_2021-03-30.tar.gz (sha256sum: b7876304ef02b3ee14c83354129c284ce239389360ee843dc6f0e85e7bd05404)
Please see the LICENSE and README files therein.

We include here also the appendix sections of the paper.
File: wr-compiler-jfp_appendices_2021-04-08.pdf (sha256sum: 2dad2765ed9b2b234bbdf9e5bbb8c041a92c4e8eaa90ffa135487f917b115ed5)

The corresponding author for this work is Robert Sison (
Future updates to this project may be posted at