Compiling high-level code to cryptography

We showed in a forthcoming paper (CSF'24) that a compiler can translate high-level sequential code into a distributed concurrent program that uses cryptography to achieve security. All source-level security properties are preserved -- robust hyperproperty preservation. This requires a new kind of compiler correctness proof based on the kind of simulation used in Universal Composability.
See Acay, Gancher, Recto, Myers, "Secure Synthesis of Distributed Cryptographic Applications".