Speaker:

   Koko Muroya (Birmingham)

Title

   A Graph-Rewriting Perspective of the Beta-Law

Abstract

   This preliminary report studies a graphical version of Plotkin's
   call-by-value equational theory, in particular its soundness with
   respect to operational semantics.  Although an equational theory is
   useful in safe program transformation like compiler optimisation,
   proving its soundness is not trivial, because it involves analysis
   of interaction between evaluation flow and a particular sub-program
   of interest.  We observe that soundness can be proved in a direct
   and generic way in the graphical setting, using small-step
   semantics given by a graph-rewriting abstract machine previously
   built for evaluation-cost analysis.  This would open up
   opportunities to think of a cost-sensitive equational theory for
   compiler optimisation, and to prove contextual equivalence directly
   in the presence of language extensions.