[isabelle] Language semantics based on graph representations
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).
This archive was generated by a fusion of
Pipermail (Mailman edition) and