Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: A Reuse-Based Multi-Stage Comp...


view this post on Zulip Email Gateway (Jul 11 2022 at 05:27):

From: Tobias Nipkow <nipkow@in.tum.de>
A Reuse-Based Multi-Stage Compiler Verification for Language IMP
Pasquale Noce

After introducing the didactic imperative programming language IMP, Nipkow and
Klein's book on formal programming language semantics (version of March 2021)
specifies compilation of IMP commands into a lower-level language based on a
stack machine, and expounds a formal verification of that compiler. Exercise 8.4
asks the reader to adjust such proof for a new compilation target, consisting of
a machine language that (i) accesses memory locations through their addresses
instead of variable names, and (ii) maintains a stack in memory via a stack
pointer rather than relying upon a built-in stack. A natural strategy to
maximize reuse of the original proof is keeping the original language as an
assembly one and splitting compilation into multiple steps, namely a
source-to-assembly step matching the original compilation process followed by an
assembly-to-machine step. In this way, proving assembly code-machine code
equivalence is the only extant task. A previous paper by the present author
introduces a reasoning toolbox that allows for a compiler correctness proof
shorter than the book's one, as such promising to constitute a further enhanced
reference for the formal verification of real-world compilers. This paper in
turn shows that such toolbox can be reused to accomplish the aforesaid task as
well, which demonstrates that the proposed approach also promotes proof reuse in
multi-stage compiler verifications.

https://www.isa-afp.org/entries/IMP_Compiler_Reuse.html

Enjoy!
smime.p7s


Last updated: Jul 15 2022 at 23:21 UTC