### Abstract

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.

### License

BSD License

### Topics

- Computer science/Programming languages/Compiling

### Session IMP_Compiler

- Compiler
- Compiler2

## Cite

×

IMP_Compiler-AFP

    @article{IMP_Compiler-AFP,
      author  = {Pasquale Noce},
      title   = {A Shorter Compiler Correctness Proof for Language IMP},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/IMP_Compiler.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Jun 21, 2021 : Isabelle2021