Thierry Coquand, Anders Mörtberg, Vincent Siles. A formal proof of Sasaki-Murao algorithm. J. Formalized Reasoning, 5(1):27-36, 2012. [doi]
@article{CoquandMS12-0, title = {A formal proof of Sasaki-Murao algorithm}, author = {Thierry Coquand and Anders Mörtberg and Vincent Siles}, year = {2012}, doi = {10.6092/issn.1972-5787/2615}, url = {http://dx.doi.org/10.6092/issn.1972-5787/2615}, researchr = {https://researchr.org/publication/CoquandMS12-0}, cites = {0}, citedby = {0}, journal = {J. Formalized Reasoning}, volume = {5}, number = {1}, pages = {27-36}, }