Compiler-compilers are tools that generate substitutes for hand-written compiler components from high-level formal specifications. Such tools exist for lexical, syntactic and semantic analysis, optimizers and code generation. The established benefits are reduced development time and increased confidence in the correctness of the resulting software.
This thesis presents a generator for type checkers. Given a description of the type system by typing rules, the generator yields a type checker that constructs proofs using the typing rules. Unlike earlier approaches, we derive suitable notions of proof and typing rule from an analysis of type systems and from corresponding constructs in mathematical proof theory. The approach thus respects the structure and intention of the typing rules, rather than expressing the rules in some pre-existing formalism.
The given applications comprise type checkers for imperative, object-oriented and functional languages, including ML type inference. The typing rules for these checkers directly represent those found in the literature. They naturally describe the typing of single language constructs and they can be re-used in different. checkers.
We use the generator to develop the language Saga for generic programming. Generic programming has become a standard approach to creating reusable and reliable software, particularly through the wide-spread use of the C++ Standard Template Library (STL). Existing C++ compilers cannot type-check generic algorithms before instances are generated, hence errors manifest themselves only when the algorithms are used.
Saga overcomes this problem by a novel language design that enables generic algorithms as found in the C++ STL to be type-checked such that the correctness requirements stated in algorithm interfaces are obeyed and instantiation never fails. It therefore turns the aims of the earlier proposal SuchThat into a concrete language design.