An Open Framework for Foundational Proof-Carrying Code Xinyu Feng Yale University Joint work with Zhaozhong Ni (Yale,now at MSR) Zhong Shao (Yale)and Yu GUo (USTC)An Open Framework for Foundational Proof-Carrying Code Xinyu Feng Yale University Joint work with Zhaozhong Ni (Yale, now at MSR), Zhong Shao (Yale) and Yu Guo (USTC)