A Language for the Specification and Efficient Implementation of Type SystemsPublished on 8.10.2015
Published in studium tu-darmstadt
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 declar- ative 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 specifica- tion: 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 auto- mated 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.