Ruler Programming Type Rules

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