Vidal, C.; Aguado, F.; Doncel, J. L.; Molinelli, J. M.; Perez, G. Genetic Algorithms in Coq: Generalization and Formalization of the Crossover Operator. JFR 2008, 1, 25-37.