Verified Compilation for Shared-Memory C

DOI10.1007/978-3-642-54833-8_7zbMath1346.68045OpenAlexW59640247MaRDI QIDQ5410696

Gordon Stewart, Andrew W. Appel, Robert Dockins, Lennart Beringer

Publication date: 16 April 2014

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-54833-8_7

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20)

Related Items (5)

Trace-Relating Compiler Correctness and Secure Compilation ⋮ A formal C memory model for separation logic ⋮ Iris from the ground up: A modular foundation for higher-order concurrent separation logic ⋮ The Essence of Higher-Order Concurrent Separation Logic ⋮ Unnamed Item

Uses Software

• Coq

This page was built for publication: Verified Compilation for Shared-Memory C