Vidal, Concepción, et al. “Genetic Algorithms in Coq: Generalization and Formalization of the Crossover Operator”. Journal of Formalized Reasoning, vol. 1, no. 1, Jan. 2008, pp. 25-37, doi:10.6092/issn.1972-5787/1052.