Andrew W. Appel. Foundational ProofCarrying Code, 16th Annual IEEE Symposium on Logic in Computer Science (LICS '01), June 2001.
Proofcarrying code is a framework for the mechanical
verification of safety properties of machine language
programs, but the problem arises of quis custodiat ipsos
custodes  who will verify the verifier itself? Foundational
proofcarrying code is verification from the smallest
possible set of axioms, using the simplest possible verifier
and the smallest possible runtime system. I will describe
many of the mathematical and engineering problems
to be solved in the construction of a foundational
proofcarrying code system.
Very interesting survey paper. As an added bonus you can see examples of using Twelf (the metalogic framework), and an interesting approach to typing (section 5.2).
Warning: This paper is pretty dense.
Posted to theory by Ehud Lamm on 12/6/01; 3:57:04 AM
