An Indexed Model of Recursive Types for Foundational Proof-Carrying Code

Abstract:

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.