Title: On using Edinburgh LCF to prove the correctness of a parsing algorithm