Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: A Shorter Compiler Correctness...

view this post on Zulip Email Gateway (Jun 21 2021 at 07:12):

From: Tobias Nipkow <>
A Shorter Compiler Correctness Proof for Language IMP
Pasquale Noce

This paper presents a compiler correctness proof for the didactic imperative
programming language IMP, introduced in Nipkow and Klein's book on formal
programming language semantics (version of March 2021), whose size is just two
thirds of the book's proof in the number of formal text lines. As such, it
promises to constitute a further enhanced reference for the formal verification
of compilers meant for larger, real-world programming languages. The presented
proof does not depend on language determinism, so that the proposed approach can
be applied to non-deterministic languages as well. As a confirmation, this paper
extends IMP with an additional non-deterministic choice command, and proves
compiler correctness, viz. the simulation of compiled code execution by source
code, for such extended language.

Last updated: Jan 25 2022 at 01:11 UTC