An formalized micro-compiler for Krivine machines

Stream: lean4

[Ryan Lahfa]

We (= @Julien Marquet and me) are happy to "release" one of our (school) project: https://github.com/RaitoBezarius/compiler9000 which is an extremely simple lambda calculus → Krivine machine certified [1] compiler [2].

We were supposed to do it in Coq, but it sounded a nice self contained project for an evaluation of Lean 4, so we convinced our teacher to let us do it in Lean 4, he accepted at one condition, to have everything without sorry by the end of the project -- it was pretty cool all the way.

We might do some stuff on the top of this if we have some time, we would like to see how far we can go with such toy models, for the theory behind this, here is a nice paper: https://drops.dagstuhl.de/opus/volltexte/2014/4634/pdf/13.pdf which proves "more" but I think the Coq proofs are definitely lost, I was not able to find them and the authors are not answering over email alas.

Thanks for the Lean 4 developers and everyone who helped and suggested solutions when we posted here. :)

[1]: Well, it does not have all the desired theorems and it would require some work but straightforward to have all the theorems one might want for such things.
[2]: Well, we did not yet tried to extract it in C/C++ as we have some unsafe definitions which are more placeholder-like than really implemented.