A Language for the Specification and Efficient Implementation of Type Systems

nischen Universität Darmstadt (APB) §23 (7), die vorliegende Masterarbeit ohne Hilfe Dritter und nur mit den angegebenen Quellen und Hilfsmitteln angefertigt zu haben. Alle Stellen, die aus den Quellen entnommen wurden, sind als solche kenntlich gemacht worden. Diese Arbeit hat in gleicher oder ähnlicher Form noch keiner Prüfungsbehörde vorgelegen. Ort, Datum (Pascal Wittmann) ii 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 theore