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

denotational semanticsPrologformal specificationcorrect compilerDCTG

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

• 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?)
• Compiler specification and verification
• Grammar Analysis and Parsing by Abstract Interpretation
• Information-flow and data-flow analysis of while-programs
• Logic programming and compiler writing
• Semantics of context-free languages

Cited in

(8)

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

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)