A demonstrably correct compiler

DOI10.1007/BF01211435MaRDI QIDQ749202zbMATH OpenOpenAlexWikidataFDO

Authors D. Kharzeev

Publication date 1991

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf01211435

zbMATH Keywords

correct compilerDCTGdenotational semanticsformal specificationProlog

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Toward compiler implementation correctness proofs
• scientific article; zbMATH DE number 578229
• Specification, verification and prototyping of an optimized compiler
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Provably correct code generation: a case study

Cites work

• Compiler specification and verification
• Grammar Analysis and Parsing by Abstract Interpretation
• scientific article; zbMATH DE number 3978351 (Why is no real title available?)
• scientific article; zbMATH DE number 3793435 (Why is no real title available?)
• scientific article; zbMATH DE number 42778 (Why is no real title available?)
• scientific article; zbMATH DE number 3483540 (Why is no real title available?)
• scientific article; zbMATH DE number 3485184 (Why is no real title available?)
• scientific article; zbMATH DE number 3640837 (Why is no real title available?)
• scientific article; zbMATH DE number 3992919 (Why is no real title available?)
• scientific article; zbMATH DE number 3291623 (Why is no real title available?)
• scientific article; zbMATH DE number 3410594 (Why is no real title available?)
• Information-flow and data-flow analysis of while-programs
• Logic programming and compiler writing
• Semantics of context-free languages

Cited in

(9)

• Deriving correctness properties of compiled code
• Specification, verification and prototyping of an optimized compiler
• Provably correct code generation: a case study
• scientific article; zbMATH DE number 1374873 (Why is no real title available?)
• scientific article; zbMATH DE number 578229 (Why is no real title available?)
• On Trojan horses of Thompson-Goerigk-type, their generation, intrusion, detection and prevention
• Calculating correct compilers
• A Completely Verified Realistic Bootstrap Compiler
• Correct hardware synthesis

This page was built for publication: A demonstrably correct compiler

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