[1]
B. Ahrens and J. Zsido, “Initial Semantics for higher-order typed syntax in Coq”, JFR, vol. 4, no. 1, pp. 25–69, Jan. 2011.