I am attempting at an Agda implementation of the MinML5 language described in the paper "Modal Types for Mobile Code", with a few changes to the language.
After the compilation of MinML5 to JavaScript, I will try to prove the correctness of the compiler.