[Prev][Next][Index][Thread]
Re: Formal semantics for C
-
To: types@cis.upenn.edu
-
Subject: Re: Formal semantics for C
-
From: Sava Krstic <krstic@cse.ogi.edu>
-
Date: Sun, 23 Dec 2001 00:53:11 -0800 (PST)
-
In-Reply-To: <200112221624.fBMGOdq04891@saul.cis.upenn.edu>
Another reference:
Nikolaos S. Papaspirou, Denotational Semantics of ANSI C. Computer
Standards and Interfaces, 23, 169--185, 2001
Sava Krstic
On 22 Dec 2001, Ken Friis Larsen wrote:
> [----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
>
> "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
>