Gale-Shapley Algorithm

Tobias Nipkow

29 December 2021


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(n2) where n is the cardinality of the two sets to be matched.
BSD License

Depends On