Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Executable Formal Semantics of C
Authors: Brian Campbell ; Robert Pollack
Date:Dec 2010
Publication Type:Other Publication Status:Other
We present an execution semantics of the C programming language for use in the CerCo project. It is based on the small-step inductive semantics used by the CompCert verified compiler. We discuss the extensions required for our target architecture, porting the semantics to our choice of tool, Matita, providing an equivalent executable semantics and the validation of the semantics.
Links To Paper
1st Link
2nd Link
Bibtex format
author = { Brian Campbell and Robert Pollack },
title = {Executable Formal Semantics of C},
year = 2010,
month = {Dec},
url = {},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh