Lambda the Ultimate

Type checking after inference is pretty straightforward and typically not too expensive, but suppose we have a low powered device that receives some mobile code. Is there some sort of even cheaper proof of work that type checking will pass, so we can avoid verifying the code's type safety?

I don't mean some cryptographic certificate requiring verification of the sender since that requires trusting the sender, but a shortcut to verifying some meaningful safety independent of any other parties. Proof-carrying code still requires verifying the code against the proof certificate, so I'm looking for something cheaper.

For instance, something like Tamper-Proof Annotations, by Construction, and the follow-up Making Mobile Code Both Safe and Efficient. Any other ideas out there?

Edit: the following seems like a good overview of various bytecode formats and their safety properties as of 2007, covering also the tamper-proof bytecodes above: Intermediate Representations of Mobile Code.