A formal proof of Sasaki-Murao algorithm

Thierry Coquand, Anders Mörtberg, Vincent Siles. A formal proof of Sasaki-Murao algorithm. J. Formalized Reasoning, 5(1):27-36, 2012. [doi]