Technical reports
A tool to support formal reasoning about computer languages
Richard J. Boulton
November 1996, 21 pages
DOI: 10.48456/tr-405
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
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 = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-405.ps.gz}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-405}, number = {UCAM-CL-TR-405} }