Compilation as Rewriting in Higher Order Logic

DOI10.1007/978-3-540-73595-3_3zbMATH Open1213.68194OpenAlexW1746660792MaRDI QIDQ3608760FDOQ3608760

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

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

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (8)

• A formally verified compiler back-end
• Trusted Source Translation of a Total Function Language
• Formal compiler construction in a logical framework
• Title not available (Why is that?)
• A Brief Overview of HOL4
• Title not available (Why is that?)
• Composing programs in a rewriting logic for declarative programming
• Code generation via higher-order rewrite systems

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)