In their paper "Algorithmic Nominal Game Semantics", which appeared
at ESOP (the 19th European Symposium on Programming) in March, Andrzej
Murawski and Nikos Tzevelekos presented an algorithmic characterisation
of a fragment of the ML language with numerical references. Their
construction comes as a culmination of a three-year long collaboration
and capitalises on major achievements of the last years in semantics of
programs with dynamic generation of resources, and in particular on
nominal game semantics and fresh-register automata.
Devising precise descriptions of higher-order programs with dynamic
generation of resources is a daunting task, especially if one is
interested in focussing just on observable behaviours. The reasons for
this complication are due to the fact that dynamic resources combined
with
|
|
higher-order functions give rise to issues of privacy and data flow
which cannot be resolved by standard analyses. A major breakthrough in
this direction has been made recently with the introduction of nominal
game semantics, a strand of the well-established theory of game
semantics which addresses generative dynamic behaviours.
Andrzej and Nikos have been instrumental, not only in developing the
theory, but also applying it towards giving algorithmic representations
of its models. In a paper which appeared in FOSSACS (the 12th International
Conference on Foundations of Software Science and Computation
Structures) in 2009, they introduced a game model of Reduced ML, a
fragment of ML with integer variables. Their model was the first such to
provide an explicit characterisation of observable program behaviour –
and it did so in a compositional denotational
|
|
manner. Moreover, the
explicitness of the description allowed for algorithmic representations
of the model, by means of abstract machines.
Primitive such machines for dynamic resource generation, called
fresh-register automata, had been recently introduced by Nikos in a
paper which appeared in POPL (the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages) earlier this year. Andrzej and Nikos further extended
these machines to capture game semantics. They were thus able to
represent their model of a non-trivial fragment of Reduced ML and thus
prove decidability of program equivalence. This is the first such result
in languages with dynamic generative features and paves the way for
algorithmic descriptions of other languages of this kind, including
fragments of Java or C#.
|
|
|