"S.J.Thompson" <S.J.Thompson@ukc.ac.uk> writes:
> Query about the formal semantics of C:
>
> Are types readers aware of any work on formalizing the semantics
> of the C programming language?
Michael Norrish (Computer Lab, University of Cambridge) developed a
formal model for C and embedded this model into the HOL theorem
prover. More information here:
http://www.cl.cam.ac.uk/users/mn200/PhD/
Cheers,
--Ken Friis Larsen