Re: [isabelle] Encoding an evaluation context



Hallo Klaus,

> I am trying to formalize a programming language semantics.
>
> Small-step semantics are frequently formalized by using an evaluation
> context which controls the order of evaluation. 
>
> What would be a good way to encode an evaluation context in Isabelle? Are
> there maybe existing examples that I could look at?
Michael Norrish discusses one solution (for HOL)
in Section 3.3.1 (and various further spots for extensions):

@PhdThesis{norrish98phd,
  author =       {Norrish, Michael},
  title =        {C formalised in {HOL}},
  school =       {University of Cambridge},
  year =         1998,
  note =         {Technical Report UCAM-CL-TR-453}
}

-- 
Holger






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.