Compilation as Rewriting in Higher Order Logic

DOI10.1007/978-3-540-73595-3_3MaRDI QIDQ3608760zbMATH OpenOpenAlexFDO

Authors Guodong Li, Konrad Slind

Publication date 6 March 2009

Published in Automated Deduction – CADE-21 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-73595-3_3

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

• Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic
• Certifying compilers using higher-order theorem provers as certificate checkers
• Proof-producing synthesis of ML from higher-order logic
• scientific article; zbMATH DE number 2079040
• Proof-producing translation of higher-order logic into pure and stateful ML

Cited in

(8)

• A formally verified compiler back-end
• A Brief Overview of HOL4
• Code generation via higher-order rewrite systems
• scientific article; zbMATH DE number 1342285 (Why is no real title available?)
• scientific article; zbMATH DE number 549957 (Why is no real title available?)
• Composing programs in a rewriting logic for declarative programming
• Trusted Source Translation of a Total Function Language
• Formal compiler construction in a logical framework

Describes a project that uses

Uses Software

• Isabelle/HOL

This page was built for publication: Compilation as Rewriting in Higher Order Logic

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