Towards Using Constructive Type Theory for Verifiable Modular Transformations
Steffen Zschaler, Iman Poernomo, Jeff Terrell · 2011
Model transformations have been studied for some time, typically using a semantics based on graph transformations. This has been very successful in defining, optimising and executing model transformations, but has been less useful for providing a firm semantic basis for modular, reusable transformations. We propose a novel rendering of transformation semantics in terms of constructive type theory and show how this can be employed for expressing dependencies and guarantees of transformation modules in a formal framework.