Nicolas Magaud, Julien Narboux, Pascal Schreck. Formalizing Desargues theorem in Coq using ranks. In Sung Y. Shin, Sascha Ossowski, editors, Proceedings of the 2009 ACM Symposium on Applied Computing (SAC), Honolulu, Hawaii, USA, March 9-12, 2009. pages 1110-1115, ACM, 2009. [doi]
Abstract is missing.