Lightweight verification of separate compilation

DOI10.1145/2837614.2837642zbMath1347.68085OpenAlexW2295752850MaRDI QIDQ2828254

Derek R. Dreyer, Yoonseung Kim, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur

Publication date: 24 October 2016

Published in: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2837614.2837642

zbMATH Keywords

separate compilationCompCertcompositional compiler verification

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Trace-Relating Compiler Correctness and Secure Compilation, The verified CakeML compiler backend