Genetic Algorithms in Coq: Generalization and Formalization of the crossover operator

Concepción Vidal, Felicidad Aguado, José Luis Doncel, Jose María Molinelli & Gilberto Perez
In this article we present the implementation and formal verification, using the Coq system, of a generalized version of the crossover operator applied to genetic algorithms (GA). The first part of this work defines the multiple crossover of two lists in any finite number of points, generalizing a previous definition by Uchibori. In the second part, we show that the definition does not depend on the order of the list of points. Then, a more...