Completed in 2019 for partial fulfilment of the Bachelor of Information Technology (Honours, Class 1) at Griffith University.
A verified, type-preserving, crossover method for well-typed higher order abstract syntax trees. This thesis discusses the use of dependently typed programming techniques, with accompanying proofs, to guarantee only well-typed crossover operations in genetic programming.