Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules (Technical Report)

Ling Zhang, Yuting Wang, Jinhua Wu +2

Verified compilation of open modules (i.e., modules whose functionality depends on other modules) provides a foundation for end-to-end verification of modular programs ubiquitous i…