Technical reports
Symbolic compilation and execution of programs by proof: a case study in HOL
Juanito Camilleri
December 1991, 31 pages
DOI: 10.48456/tr-240
Abstract
This paper illustrates the symbolic compilation and execution of programs by proof using the proof assistant HOL. We formalise the operational semantics of an Occam-like programming language oc and show how synchronous communication in oc compiles to an intermediate programming language Safe, whose compilation yields instructions intended to drive machines that communicate via shared memory. We show how the symbolic formal manipulation of terms of a programming language, subject to the definition of its semantics, can animate a desired effect — be it compilation or execution. Needless to say, such compilation and execution by proof is rather slow, but it is fast enough to give vital feedback about the compilation algorithm being used. Without such animation it is hard to anticipate whether the compilation algorithm is reasonable before attempting to verify it. This is particularly true when attempting to find a plausible handshaking protocol that implements synchronous communication.
Full text
PDF (1.9 MB)
BibTeX record
@TechReport{UCAM-CL-TR-240, author = {Camilleri, Juanito}, title = {{Symbolic compilation and execution of programs by proof: a case study in HOL}}, year = 1991, month = dec, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-240.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-240}, number = {UCAM-CL-TR-240} }