Formalizing Stalmarck's algorithm in Coq

International audienceWe present the development of a machine-checked implementation of Stalmarck's algorithm. First, we prove the correctness and the completeness of an abstract representation of the algorithm. Then, we give an effective implementation of the algorithm that we prove correct