A verified Implementation of a mini prolog
- Formalize the semantics of Prolog
- A purely logical semantics
- An operational semantics
- Prove the equivalence of the 2 semantics
- Verify an executable prolog interpreter in Coq
- Verified matching algorithm
- Verified unification algorithm