Computer Laboratory

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}
}