Computer Laboratory

Technical reports

A tool to support formal reasoning about computer languages

Richard J. Boulton

November 1996, 21 pages

Abstract

A tool to support formal reasoning about computer languages and specific language texts is described. The intention is to provide a tool that can build a formal reasoning system in a mechanical theorem prover from two specifications, one for the syntax of the language and one for the semantics. A parser, pretty-printer and internal representations are generated from the former. Logical representations of syntax and semantics, and associated theorem proving tools, are generated from the combination of the two specifications. The main aim is to eliminate tedious work from the task of prototyping a reasoning tool for a computer language, but the abstract specifications of the language also assist the automation of proof.

Full text

PS (0.1 MB)
DVI (0.0 MB)

BibTeX record

@TechReport{UCAM-CL-TR-405,
  author =	 {Boulton, Richard J.},
  title = 	 {{A tool to support formal reasoning about computer
         	   languages}},
  year = 	 1996,
  month = 	 nov,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-405.ps.gz},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-405}
}