Technical reports
An abstract dynamic semantics for C
Michael Norrish
May 1997, 31 pages
DOI: 10.48456/tr-421
Abstract
This report is a presentation of a formal semantics for the C programming language. The semantics has been defined operationally in a structured semantics style and covers the bulk of the core of the language. The semantics has been developed in a theorem prover (HOL), where some expected consequences of the language definition
Full text
PDF (0.2 MB)
PS (0.1 MB)
DVI (0.0 MB)
BibTeX record
@TechReport{UCAM-CL-TR-421, author = {Norrish, Michael}, title = {{An abstract dynamic semantics for C}}, year = 1997, month = may, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-421.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-421}, number = {UCAM-CL-TR-421} }