Lambda the Ultimate

inactiveTopic Foundational Proof-Carrying Code
started 12/6/2001; 3:55:59 AM - last post 12/6/2001; 3:55:59 AM
Ehud Lamm - Foundational Proof-Carrying Code  blueArrow
12/6/2001; 3:55:59 AM (reads: 1557, responses: 0)
Foundational Proof-Carrying Code
Andrew W. Appel. Foundational Proof-Carrying Code, 16th Annual IEEE Symposium on Logic in Computer Science (LICS '01), June 2001.

Proof-carrying 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 proof-carrying 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 proof-carrying 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