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