Published on *Computer Science Department at Princeton University* (http://www.cs.princeton.edu)

The proofs of ``traditional'' proof carrying code (PCC) are type-specialized

in the sense that they require axioms about a specific type system.

In contrast, the proofs of foundational PCC explicitly define all required

types and explicitly prove all the required properties of those types

assuming only a fixed foundation of

mathematics such as higher-order logic.

Foundational PCC is both more flexible and

more secure than type-specialized PCC.For foundational PCC we need semantic models of type systems on

von Neumann machines.

Previous models have been either too weak

(lacking general recursive types and first-class function-pointers),

too complex (requiring machine-checkable proofs of large bodies

of computability theory), or not obviously applicable to von Neumann

machines. Our new model is strong, simple, and works either in

lambda-calculus or on Pentiums.