Technical reports
On using Edinburgh LCF to prove the correctness of a parsing algorithm
Avra Cohn, Robin Milner
February 1982, 23 pages
DOI: 10.48456/tr-20
Abstract
The methodology of Edinburgh LCF, a mechanized interactive proof system is illustrated through a problem suggested by Gloess – the proof of a simple parsing algorithm. The paper is self-contained, giving only the relevant details of the LCF proof system. It is shown how tactics may be composed in LCF to yield a strategy which is appropriate for the parser problem but which is also of a generally useful form. Also illustrated is a general mechanized method of deriving structural induction rules within the system.
Full text
PDF (1.2 MB)
BibTeX record
@TechReport{UCAM-CL-TR-20, author = {Cohn, Avra and Milner, Robin}, title = {{On using Edinburgh LCF to prove the correctness of a parsing algorithm}}, year = 1982, month = feb, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-20.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-20}, number = {UCAM-CL-TR-20} }