Technical reports

The correctness of a precedence parsing algorithm in LCF

A. Cohn

April 1982, 38 pages

DOI: 10.48456/tr-21

Abstract

This paper describes the proof in the LCF system of a correctness property of a precedence parsing algorithm. The work is an extension of a simpler parser and proof by Cohn and Milner (Cohn & Milner 1982). Relevant aspects of the LCF system are presented as needed. In this paper, we emphasize (i) that although the current proof is much more complex than the earlier one, mqany of the same metalanguage strategies and aids developed for the first proof are used in this proof, and (ii) that (in both cases) a general strategy for doing some limited forward search is incorporated neatly into the overall goal-oriented proof framework.

Full text

PDF (1.8 MB)

BibTeX record

@TechReport{UCAM-CL-TR-21,
  author =	 {Cohn, A.},
  title = 	 {{The correctness of a precedence parsing algorithm in LCF}},
  year = 	 1982,
  month = 	 apr,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-21.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-21},
  number = 	 {UCAM-CL-TR-21}
}