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

DOI10.1007/978-3-540-71316-6_15zbMATH Open1187.68141OpenAlexW1536568106MaRDI QIDQ5756497FDOQ5756497

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

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

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20)

Cited In (7)

• A formally verified compiler back-end
• Adapting functional programs to higher order logic
• Formal Certification of a Resource-Aware Language Implementation
• Verified compilation of floating-point computations
• Proof-producing synthesis of ML from higher-order logic
• Title not available (Why is that?)
• 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)