3rd BCS-FACS Northern Formal Methods Workshop (NFM)
BCS-FACS Northern Formal Methods Workshop
14-15 September 1998
This paper describes work leading towards the concept of a Geometry of Formal Methods[Mac96],[HM97], which explores the relationship between various formal description techniques and aspects of modern abstract algebraic theories with a strong geometric interpretation, in particular such concepts as fibre-bundles, sheaves and related ideas in topology and category theory. Inspired by ideas and notions of seeking a geometry of computing and of formal methods, and with the category theoretic concepts of topos in mind, we explore how such a geometry might be expressed in concrete diagrams, and explore their ability to lay clear some of the concepts behind tail recursion optimisation. We also indicate how this approach can be used in an exposition of various published program transformation rules in this area. We also show the use of category theoretic notions to help explain the similarity of two apparently quite different diagrams. All of this points towards a future foundation for our geometry, both in diagrammatic and algebraic form, in the area of category theory.