A minimalistic verified bootstrapped compiler (proof pearl)

Abstract

This paper shows how a small verified bootstrapped compiler can be developed inside an interactive theorem prover (ITP). Throughout, emphasis is put on clarity and minimalism.