Department of Computer Science and Technology

Technical reports

An abstract dynamic semantics for C

Michael Norrish

May 1997, 31 pages

DOIhttps://doi.org/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}
}