Ruler: Programming Type Rules

  • Atze Dijkstra, S. Doaitse Swierstra, 2006
  • in LNCS FLOPS 2006 proceedings of FLOPS 2006
  • Abstract: Some type systems are first described formally, to be sometimes followed by an implementation. Other type systems are first implemented as language extensions, to be sometimes retrofitted with a formal description. In neither case it is an easy task to keep both artefacts consistent. In this paper we introduce Ruler, a domain specific language for describing type rules. Type rules can be incrementally described, thus providing a means for building complex type systems on top of simpler ones. Besides checking well-formedness of Ruler programs we use them to generate (1) a visual LATEX rendering, suitable for use in the presentation of formal aspects, and (2) an attribute grammar based implementation. Combining these two aspects in Ruler contributes to bridging the gap between theory and practice: mutually consistent representations can be generated for use in both theoretical and practical settings.

-- AtzeDijkstra - 21 Sep 2007
Topic revision: r2 - 27 Nov 2007, UnknownUser

This site is powered by FoswikiCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding UUCS? Send feedback