Important
This repository has been moved from GitHub to Codeberg (https://codeberg.org/pSub/master-thesis). The GitHub repository is archieved will no longer receive updates. Please update your bookmarks and clones accordingly.
Type systems are important tools to detect semantic inconsistencies, to establish abstractions and to guide programmers in the development process. However, there is currently a lack of established tools supporting the development of type systems, tools like lexer and parser generators but for type systems. We introduce a declarative specification language for type systems that allows to specify type systems in a natural deductive style. We generate two products out of a type system specification: A first-order formula representation to facilitate the use of automated theorem provers and a type checker. The type checker generator uses results proven by automated theorem provers to check the applicability of optimization strategies and the first-order formula representation is also a reference implementation. Both results aim to accelerate the development cycle for type systems and to narrow the gap between theory and practice.
* Clone repository
* Install vampire and make sure it is in PATH
* Install Eclipse plugin Spoofax (https://spoofax.dev/getting-started/)
* Import project into Eclipse
* Build the project to make sure everything works
* Restart Eclipse
* Choose a type system from the folder syntax/specification/
* Comment all lines after `rules`
* Click on `Generation` -> `Generate SDF`
* Build the project again
* Uncomment the lines after `rules`
Now you are ready to select actions from the Typecheck and
Verification menus, add new typing rules and conjectures. Changes in
the sections meta-variables, contexts and judgments require the
regeneration of the sdf file and a rebuild of the project.