Mobile programs can potentially be malicious. To protect itself, a host that receives such mobile programs from an untrusted party or via an untrusted network connection will want some kind of guarantee that the mobile code is not about to cause any damage. The traditional solution to this problem has been verification, by which the receiving host examines the mobile program to discover all its actions even before starting execution. Unfortunately, aside from consuming computing resources in itself, verification inhibits traditional compiler optimizations, making such verifiable mobile code much less efficient than native code.

We have found an alternative solution by identifying a class of mobile-code representations in which malicious programs can simply not be encoded to begin with. In such an encoding, verification turns into an integral part of the decoding routine. Moreover, support for high-quality just-in-time code generation can be provided. We present two such encodings, one based on highly effective compression of abstract syntax trees, and another based on a reference-safe and type-safe variant of Static Single Assignment form.