Conclusion

Abstract

In this thesis, we have developed a theory of models of sharing graphs arising from graph rewriting theory. Generalizing the traditional theory-model correspondence between algebraic theories and finite product preserving functors, we have established the connection between theories for sharing graphs and their models described in terms of symmetric monoidal categories, strict symmetric monoidal functors and additional requirements (adjunctions, and traces). As an important case study, we have looked at recursive computation modeled in our higher-order cyclic sharing theories and their models. Also we have shown that Milner’s action calculi can be understood in terms of our sharing theories enriched with parametrized operators. As an interesting implication, our axiomatic treatment of the classes of models has enabled us to compare them with those for related theories, including Moggi’s notions of computation as well as intuitionistic linear type theory.