SCS Undergraduate Thesis Topics

Student Advisor Thesis Topic
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.

Close this window