Project

Compilation Using Correct-by-Construction Program Synthesis

We're using proof assistants to build correct, extensible compilers, by rephrasing compilation in terms of producing mathematical proofs.