Ahrens, B. and Zsido, J. 2011. Initial Semantics for higher-order typed syntax in Coq. Journal of Formalized Reasoning. 4, 1 (Jan. 2011), 25–69. DOI:https://doi.org/10.6092/issn.1972-5787/2066.