Technical reports

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

**Avra Cohn, Robin Milner**

February 1982, 23 pages

## 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 = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-20.pdf}, institution = {University of Cambridge, Computer Laboratory}, number = {UCAM-CL-TR-20} }