3 ms·
Seriously amazing work. Formally verified compiler for a functional language down, with support for exceptions, GC, bignums, ... down to 5 different architectu
by ghettoimp 8y ago
Seriously amazing work. Formally verified compiler for a functional language down, with support for exceptions, GC, bignums, ... down to 5 different architectures, including x86 and ARM. Carried out in HOL4.