A Language for the Specification and Efficient Implementation of Type Systems

Published 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.



Leave a Reply


Kommentare für diesen Eintrag als RSS Feed
Anonymous on 7.12.2022 wrote Reply

Make money trading opions. The minimum deposit is 50$. Learn how to trade correctly. How to earn from $50 to $5000 a day. The more you earn, the more profit we get.

binary option strategies 2013 nfl