Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic
From MaRDI portal
Publication:5756497
DOI10.1007/978-3-540-71316-6_15zbMath1187.68141MaRDI QIDQ5756497
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
68N20: Theory of compilers and interpreters
Related Items
Adapting functional programs to higher order logic, Verified compilation of floating-point computations, A formally verified compiler back-end, Formal Certification of a Resource-Aware Language Implementation