It is well known one can compile higher order abstract syntax to a closed cartesian category. This project flips the arrows compiling the higher order abstract syntax to the categorical dual. I'm not sure of the best interpretation of a category but I eventually settled on trying to make it work something like a logic programming languaage.