Magnus O. Myreen: A minimalistic verified bootstrapped compiler (proof pearl). CPP 2021: 32-45