Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic

DOI10.1007/978-3-540-71316-6_15MaRDI QIDQ5756497zbMATH OpenOpenAlexFDO

Authors Guodong Li, Scott Owens, Konrad Slind

Publication date 4 September 2007

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

Full work available at URL https://doi.org/10.1007/978-3-540-71316-6_15

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20)

Recommendations

• scientific article; zbMATH DE number 4053062
• scientific article; zbMATH DE number 1420805
• An improved proof-theoretic compilation of logic programs
• Proof-theoretic and higher-order extensions of logic programming
• scientific article; zbMATH DE number 1617310
• Theorem provers for substructural logics
• scientific article; zbMATH DE number 1696789
• Proof-producing synthesis of ML from higher-order logic
• Formal compiler construction in a logical framework
• A verified proof checker for higher-order logic

Cited in

(7)

• Adapting functional programs to higher order logic
• Proof-producing synthesis of ML from higher-order logic
• scientific article; zbMATH DE number 2079040 (Why is no real title available?)
• A formally verified compiler back-end
• Verified compilation of floating-point computations
• Formal Certification of a Resource-Aware Language Implementation
• Compilation as Rewriting in Higher Order Logic

This page was built for publication: Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic

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