Advertisement
Published in:
2007 | OriginalPaper | Chapter
Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic
Authors : Guodong Li, Scott Owens, Konrad Slind
Published in: Programming Languages and Systems
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
We give an overview of a proof-producing compiler which translates recursion equations, defined in higher order logic, to assembly language. The compiler is implemented and validated with a mix of translation validation and compiler verification techniques. Both the design of the compiler and its mechanical verification are implemented in the same logic framework.