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

DOI10.1007/978-3-540-71316-6_15zbMath1187.68141OpenAlexW1536568106MaRDI 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

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20)

Related Items (4)

Formal Certification of a Resource-Aware Language Implementation ⋮ A formally verified compiler back-end ⋮ Adapting functional programs to higher order logic ⋮ Verified compilation of floating-point computations

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