Let's boost λProlog to implement an elaborator for CIC!
λProlog and the Calculus of Inductive Constructions
Embeddable Lambda Prolog Interpreter
LPCIC
Coq plugin embedding elpi
