[isabelle] Language semantics based on graph representations



Hi,

In the tutorial and - if I recall correctly -  the "Winskel is right (almost)" 
literature there are examples of programming language semantics where the 
abstract syntax is defined using datatype constructors.

Giving a semantics to a language that uses mutually recursive datatypes to 
represent commands, arithmetic and Boolean expressions seems relatively 
straight-forward using these as references.  On the other hand, I'm looking 
for semantics of graph-based representations of a program.

I'm aware of Jan Olaf Blech's dissertation that gives a semantics of a DAG 
representation by converting the DAG into a number of trees, but I'd be 
grateful if anyone has any pointers to other approaches to this problem in 
either Isabelle/HOL or HOL?

(Actually, perhaps giving a semantics to a representation that uses a set of 
(nodes,edges) might not be so hard, but doing anything useful with it seems 
rather difficult to me - although I confess I haven't actually tried it).

Thanks
Martin





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