Compiler verification meets cross-language linking via data abstraction
Compiler verification meets cross-language linking via data abstraction is a scholarly work, published in 2014. The main subjects of the publication include lock, Hoare logic, interprocedural optimization, dead code elimination, program analysis, optimizing compiler, computer science, programming language, compiler, correctness, object code, Compiler correctness, axiomatic semantics, programming language semantics, operational semantics, denotational semantics, and formal methods. The authors describe the authors' Coq verification of a compiler for a high-level language, such that the compiler correctness theorem allows us to derive partial-correctness Hoare-logic theorems for programs built by linking the assembly code output by the authors' compiler and assembly code produced by other means.