An Experiment with the Boyer-Moore Theorem Prover: A Proof of the Correctness of a Simple Parser of Expressions.

Paul Y. Gloess

Browse the full CADE paper archive.