SCS Undergraduate Thesis Topics
|Brandon Bohrer||Karl Crary||Certifying Compilations for Logic Programming|
We seek a certifying compiler for logic programs (in a core subset of Prolog), meaning a compiler whose output provably implements the source program. We present a dependently-typed virtual machine based on the Warren Abstract Machine (WAM), prove soundness and completeness of the VM, and implement a compiler that targets it. We then demonstrate how the type system is expressive enough to encode the correctness of the compiled program.