Certifying compilation and run-time code generation

DOI10.1023/A:1010039502678MaRDI QIDQ1974452zbMATH OpenFDO

Authors Luke Hornof, Trevor Jim

Publication date 6 April 2003

Published in Higher-Order and Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/A:1010039502678

zbMATH Keywords

certifying compilerrun-time code generation

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20)

Recommendations

• scientific article; zbMATH DE number 1746459
• Certificate Translation for Optimizing Compilers
• Certifying compilers using higher-order theorem provers as certificate checkers
• Verified bytecode verification and type-certifying compilation

Cited in

(16)

• Synthesizing JIT compilers for in-kernel DSLs
• A self-certifying compilation framework for WebAssembly
• An Introduction to Certificate Translation
• Symbolic transfer function-based approaches to certified compilation
• Certified complexity (CerCo)
• Certifying assembly programs with trails
• Certificate Translation for Optimizing Compilers
• Compiling for template-based run-time code generation
• scientific article; zbMATH DE number 1746459 (Why is no real title available?)
• scientific article; zbMATH DE number 2165694 (Why is no real title available?)
• scientific article; zbMATH DE number 2090151 (Why is no real title available?)
• scientific article; zbMATH DE number 2090308 (Why is no real title available?)
• A certified framework for compiling and executing garbage-collected languages
• Statically safe program generation with SafeGen
• Certifying compilers using higher-order theorem provers as certificate checkers
• \textsc{Mnemonics}: type-safe bytecode generation at run time

This page was built for publication: Certifying compilation and run-time code generation

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