Proof-carrying code is a framework for proving the safety of machine-language programs with a machine-checkable proof. Previous PCC frameworks have defined type-checking rules as part of the logic. We show a universal type framework for proof-carrying code that will allow a code producer to choose a programming language, prove the type rules for that language as lemmas in higher-order logic, then use those lemmas to prove the safety of a particular program. We show how to handle traversal, allocation, and initialization of values in a wide variety of types, including functions, records, unions, existentials, and covariant recursive types.
|Original language||English (US)|
|Number of pages||11|
|Journal||Conference Record of the Annual ACM Symposium on Principles of Programming Languages|
|State||Published - Dec 3 2000|
|Event||POPL'00 - The 27th ACM SIGPLAN-SIGACT Symposium on Principles og Programming Languages - Boston, MA, USA|
Duration: Jan 19 2000 → Jan 21 2000
All Science Journal Classification (ASJC) codes