Last modified: Sat Apr 9 03:11:32 2016 GMT.
Foundational proofs, however, are much harder to construct. Previous efforts on FPCC all required building sophisticated semantic models for types. Furthermore, none of them can be easily extended to support mutable fields and higher-order polymorphism. In this article, we present a syntactic approach to FPCC that avoids all of these difficulties. Under our new scheme, the foundational proof for a typed machine program simply consists of the typing derivation plus the formalized syntactic soundness proof for the underlying type system. The former can be readily obtained from a type-checker while the latter is known to be much easier to construct than the semantic soundness proofs. We give a translation from a typed assembly language into FPCC and demonstrate the advantages of our new system via an implementation in the Coq proof assistant.