The FLINT Project








A Compositional Semantics for Verified Separate Compilation and Linking

Last modified: Sun Dec 28 17:04:49 2014 GMT.


Tahina Ramananandro
Zhong Shao
Shu-Chun Weng
Jérémie Koenig
Yuchen Fu


Recent ground-breaking efforts such as CompCert have made a convincing case that mechanized verification of the compiler correctness for realistic C programs is both viable and practical. Unfortunately, existing verified compilers can only handle whole programs---this severely limits their applicability and prevents the linking of verified C programs with verified external libraries. In this paper, we present a novel compositional semantics for reasoning about open modules and for supporting verified separate compilation and linking. Our key idea is to replace external function calls with explicit events in the behavioral semantics. We develop a verified linking operator that makes lazy substitution on (potentially reacting) behaviors by replacing each external function call event with a behavior simulating the requested function. Finally, we show how our new semantics can be applied to build a refinement infrastructure that supports both vertical composition and horizontal composition.


In Proc. 4th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP'15), Mumbia, India, pages 3-14, January 2015.
  • Conference Paper [PDF]
  • Extended Technical Report [PDF]
  • Coq proofs, gzipped tar file: [tgz]

Copyright © 1996-2023 The FLINT Group <flint at cs dot yale dot edu>
Yale University Department of Computer Science
Validate this page