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):

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


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