We 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.
CITATION STYLE
Letouzey, P., & Thery, L. (2000). Formalizing stalmarck’s algorithm in coq. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1869, pp. 388–405). Springer Verlag. https://doi.org/10.1007/3-540-44659-1_24
Mendeley helps you to discover research relevant for your work.