Compositional CompCert

DOI10.1145/2676726.2676985MaRDI QIDQ2819813zbMATH OpenOpenAlexFDO

Authors Gordon Stewart, Lennart Beringer, Santiago Cuellar, Andrew W. Appel

Publication date 29 September 2016

Published in Proceedings of the 42nd 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/2676726.2676985

zbMATH Keywords

CompCertcompiler correctness

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20)

Recommendations

• Aspects of compositionality
• scientific article; zbMATH DE number 1507204
• Compositional reasoning
• Compositional calculus
• On compositional modelling
• Remarks on compositionality
• The representation of composition structures
• Compositional computational reflection

Cited in

(16)

• A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
• Foreword to the special focus on formal proofs for mathematics and computer science
• CompCert
• Verified software units
• Lightweight verification of separate compilation
• Compositories and Gleaves
• Composition Check Codes
• The verified CakeML compiler backend
• Linear capabilities for fully abstract compilation of separation-logic-verified code
• Trace-relating compiler correctness and secure compilation
• Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
• ANF preserves dependent types up to extensional equality
• Compiling with classical connectives
• Compiling sandboxes: formally verified software fault isolation
• Fully Abstract and Robust Compilation
• Verifying peephole rewriting in SSA compiler IRs

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Compositional CompCert

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2819813)