Verified Compiler

Stream: Lean for teaching

[Marcus Rossel]

I wrote a small self-contained verified compiler for a toy language which was intended to be used for a course, but never was. Thought I would leave it here in case this is useful for anyone else:
https://github.com/marcusrossel/verified-compiler