A semantic model of types and machine instructions for proof-carrying code

Andrew W. Appel, Amy P. Felty

Research output: Contribution to journalConference articlepeer-review

93 Scopus citations


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 languageEnglish (US)
Pages (from-to)243-253
Number of pages11
JournalConference Record of the Annual ACM Symposium on Principles of Programming Languages
StatePublished - 2000
EventPOPL'00 - The 27th ACM SIGPLAN-SIGACT Symposium on Principles og Programming Languages - Boston, MA, USA
Duration: Jan 19 2000Jan 21 2000

All Science Journal Classification (ASJC) codes

  • Software


Dive into the research topics of 'A semantic model of types and machine instructions for proof-carrying code'. Together they form a unique fingerprint.

Cite this