Stable Matching

Peter Gammie 🌐

October 24, 2016

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


We mechanize proofs of several results from the matching with contracts literature, which generalize those of the classical two-sided matching scenarios that go by the name of stable marriage. Our focus is on game theoretic issues. Along the way we develop executable algorithms for computing optimal stable matches.


BSD License


Session Stable_Matching