Composable Type System Specification using Heterogeneous Scope Graphs
Date: Wed, January 27, 2021
Room: Eelco's Zoom Room
Note: This is a MSc thesis defense
Static Analysis is of indispensable value for the robustness of software systems and the efficiency of developers. Moreover, many modern-day software systems are composed of interacting subsystems developed using different programming languages. However, in most cases no static validation of these interactions is applied.
In this thesis, we identify the Cross-Language Static Semantics Problem, which is defined as “How to provide a formal and executable specification of the static semantics of interactions between parts of a software system written in different languages.” We investigate current solutions to this problem, and propose criteria to which an all-encompassing solution to this problem must adhere.
After that, we present a design pattern for the Statix meta-DSL for static semantics specification that allows to model loosely coupled, composable type system specifications. This pattern entails that the semantic concepts of a particular domain are encoded in an interface specification library, which is integrated in the type system of concrete languages. This allows controlled but automated composition of type systems. We show that, under some well-formedness criteria, the system provides correct results.
A runtime executing composed specifications is implemented using PIE pipelines for partial incrementality, and integrated in the command-line interface and Eclipse IDE platforms, using the Spoofax 3 Framework. This allows using multi-language analysis in concrete projects.
This design pattern, and the accompanying runtime are validated using two case studies. These case studies show that the approach is effective, even in a case where there is an impedance mismatch in the data models of the involved languages.
| Composable Type System Specification using Heterogeneous Scope Graphs
Next: | Implementing the Decomposition of Soundness Proofs of Abstract Interpreters in Coq