Toward compiler implementation correctness proofs

DOI10.1145/5397.30847MaRDI QIDQ3719796zbMATH OpenOpenAlexWikidataFDO

Authors Laurian M. Chirica, David Martin

Publication date 1986

Published in ACM Transactions on Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL http://www.acm.org/pubs/contents/journals/toplas/1986-8/

zbMATH Keywords

attribute grammarscompilercompiler specificationcorrectnessimplementationparse-driven implementationssyntax-directed specificationtranslation invariants

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1374873
• scientific article; zbMATH DE number 3947597
• scientific article; zbMATH DE number 3898208
• scientific article; zbMATH DE number 3846848
• Specification, verification and prototyping of an optimized compiler

Cited in

(22)

• Specification, verification and prototyping of an optimized compiler
• A formally verified compiler back-end
• The WAM case study: Verifying compiler correctness for Prolog with KIV
• Pilsner: a compositionally verified compiler for a higher-order imperative language
• scientific article; zbMATH DE number 3846848 (Why is no real title available?)
• scientific article; zbMATH DE number 3898208 (Why is no real title available?)
• scientific article; zbMATH DE number 1374873 (Why is no real title available?)
• scientific article; zbMATH DE number 702367 (Why is no real title available?)
• scientific article; zbMATH DE number 1023019 (Why is no real title available?)
• scientific article; zbMATH DE number 1543049 (Why is no real title available?)
• Proving the correctness of behavioural implementations
• Proving correctness of compilers using structured graphs
• Proving correctness of compiler optimizations by temporal logic
• Deriving a compiler from an operational semantics written in VDL
• On Trojan horses of Thompson-Goerigk-type, their generation, intrusion, detection and prevention
• Calculating correct compilers
• A Completely Verified Realistic Bootstrap Compiler
• A demonstrably correct compiler
• One approach to the specification and verification of translators
• Correctness of static flow analysis in continuation semantics
• Providing a formal linkage between MDG and HOL
• A short proof of the lexical addressing algorithm

This page was built for publication: Toward compiler implementation correctness proofs

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