Gale-Shapley Algorithm

This is a stepwise refinement and proof of the Gale-Shapley stable matching (or marriage) algorithm down to executable code. Both a purely functional implementation based on lists and a functional implementation based on efficient arrays (provided by the Collections Framework in the AFP) are developed. The latter implementation runs in time O(n²) where n is the cardinality of the two sets to be matched.