Gale-Shapley Algorithm

Tobias Nipkow 🌐

December 29, 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


Theories of Gale_Shapley