Verifying an Open Compiler Using Multi-language Semantics

DOI10.1007/978-3-642-54833-8_8MaRDI QIDQ5410697zbMATH OpenOpenAlexDBLPWikidataFDO

Authors James T. Perconti, Amal Ahmed

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_8

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Leveraging compiler intermediate representation for multi- and cross-language verification
• A verifying compiler for a multi-threaded object-oriented language
• scientific article; zbMATH DE number 1374873
• scientific article; zbMATH DE number 1630130
• scientific article; zbMATH DE number 1956470

Cited in

(8)

• Equational logic and categorical semantics for multi-languages
• On multi-language abstraction. Towards a static analysis of multi-language programs
• ANF preserves dependent types up to extensional equality
• Compiling with classical connectives
• A verifying compiler for a multi-threaded object-oriented language
• Bialgebraic reasoning on higher-order program equivalence
• On multi-language abstraction: towards a static analysis of multi-language programs
• Leveraging compiler intermediate representation for multi- and cross-language verification

This page was built for publication: Verifying an Open Compiler Using Multi-language Semantics

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