Validating the Meta-Theory of Programming Languages (Short Paper)

摘要

We report on work in progress in building an environment for the validation of the meta-theory of programming languages artifacts, for example the correctness of compiler translations; the basic idea is to couple property-based testing with binders-aware functional programming as the meta-language for specification and testing. Treating binding signatures and related notions, such as new names generation, α-equivalence and capture-avoiding substitution correctly and effectively is crucial in the verification and validation of programming language (meta)theory. We use Haskell as our meta-language, since it offers various libraries for both random and exhaustive generation of tests, as well as for binders. We validate our approach on benchmarks of mutations presented in the literature and some examples of code "in the wild". In the former case, not only did we very quickly (re)discover all the planted bugs, but we achieved that with very little configuration effort with comparison to the competition. In the second case we located several simple bugs that had survived for years in publicly available (academic) code. We believe that our approach adds to the increasing evidence of the usefulness of property-based testing for semantic engineering of programming languages, in alternative or prior to full verification.