Dependent Types and Goal-Oriented DSMLs

Posted on July 28, 2015

Categories: idris, phd, paper

I submitted a paper entitled Using Dependent Types to Build Domain Specific Goal-Oriented Modelling Languages to GPCE '15. Sadly it was rejected. I have decided to uploaded it here, warts and all, so that it is a least indexable by the great machine spirit in the web---Hallowed be thy API.

The abstract is:

The Goal Requirements Language (GRL) has been used as a host language for the creation of Domain Specific Goal-Oriented Modelling Languages (DSMLs). The pictorial language constructs, however, do not allow for a more formal language-driven treatment to be given for DSMLs created in the GRL. Dependent types allow for more precise reasoning to be made about programs. This paper describes the GStar framework that uses of dependent types to reason on the construction of DSMLs based on the GRL. Two styles of DSML construction are presented. The first allows for structurally equivalent DSML to be created that differ in terminology and semantic constructs. The second facilitates the construction of structurally different DSMLs that have the same evaluation semantics. Both techniques allows for a direct correspondence to be made between the semantics and structure of the host language and domain language.

Constructive comments and suggestions are welcome. This paper introduces several techniques that I have developed as part of my PhD work in creating machine-checkable design patterns.