Gale-Shapley Algorithm

Tobias Nipkow 🌐

December 29, 2021

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

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

Topics

Theories of Gale_Shapley