Index of /ports/math/isabelle/work/Isabelle2005/src/ZF/IMP

      Name                    Last modified       Size  Description


[DIR] Parent Directory        09-Aug-2008 06:10      -  
[   ] Com.thy                 17-Jun-2005 07:15     5k  
[TXT] Com.thy.html            09-Aug-2008 06:10     0k  
[   ] Denotation.thy          17-Jun-2005 07:15     2k  
[TXT] Denotation.thy.html     09-Aug-2008 06:10     0k  
[   ] Equiv.thy               17-Jun-2005 07:15     2k  
[TXT] Equiv.thy.html          09-Aug-2008 06:10     0k  
[   ] ROOT.ML                 30-May-2000 07:09     1k  
[TXT] ROOT.ML.html            09-Aug-2008 06:10     0k  
[DIR] document/               09-Aug-2008 06:10      -
ZF/IMP/README

IMP -- A while-language and two semantics

The formalization of the denotational and operational semantics of a simple while-language together with an equivalence proof between the two semantics. The whole development essentially formalizes/transcribes chapters 2 and 5 of 

@book{Winskel,
 author = {Glynn Winskel},
 title = {The Formal Semantics of Programming Languages},
 publisher = {MIT Press},
 year = 1993}.

There is a report by Lötzbeyer and Sandner.

A much extended version of this development is found in HOL/IMP.