Author: Zhong Shao
Title: The Essence of Proof-Carrying Code
Abstract: 
Proof-Carrying Code (PCC) is a very general framework that can, in
principle, be used to verify arbitrary properties of machine language
programs. Existing PCC systems, including Foundational Proof-Carrying
Code (FPCC), however, have not fulfilled such promises. In this talk,
we contemplate the important principles that embody the essence of PCC
and FPCC, describe a framework that satisfies these principles, and
show that the new framework is simpler, more general and flexible, and
more likely to help us realize the full potential of PCC.