Text size
  • Small
  • Medium
  • Large
Contrast
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    Recursion Diagrams: Ideas for a Geometry of Formal Methods

    3rd BCS-FACS Northern Formal Methods Workshop

    Ilkley, UK. 14th - 15th September 1998

    AUTHORS

    Dr. A. Butterfield

    ABSTRACT

    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.

    PAPER FORMATS

    PDF filePDF Version of this Paper (348kb)