We introduce a generic framework for proof carrying code, developed and mechanically verified in Isabelle/HOL. The framework defines and proves sound a verification condition generator with minimal assumptions on the underlying programming language, safety policy, and safety logic. We demonstrate its usability for prototyping proof carrying code systems by instantiating it to a simple assembly language with procedures and a safety policy for arithmetic overflow.

@inproceedings{WildmoserNKN-TCS04,
  author="Martin Wildmoser and Tobias Nipkow and Gerwin Klein and Sebastian Nanz",
  title="Prototyping Proof Carrying Code",
  booktitle="Proc.\ TCS 3rd Int.\ Conf.\ on Theoretical Computer Science (TCS2004)",
  publisher="Kluwer Academic Publishers",
  month=Aug,
  year=2004,
  editor="Jean-Jacques Levy and Ernst W. Mayr and John C. Mitchell",
  pages="333--347", 
}