Ahrens, B.; Zsido, J. Initial Semantics for Higher-Order Typed Syntax in Coq. JFR 2011, 4, 25-69.