一句话：提出类型与效应系统保守检测求值顺序依赖，并据此生成程序以差分测试 OCaml 编译器后端。
如何用 QuickCheck（基于属性的测试）测试语言实现？按语法生成程序时，静态类型语言（如 OCaml）中大量候选程序会被类型检查器拒绝。已有工作按类型关系自底向上目标导向生成良类型程序，但生成程序常依赖未充分规定的求值顺序，如 OCaml、Scheme、C、C++ 等。本文提出类型与效应系统，保守检测表达式是否依赖求值顺序，并将其目标导向解读作为程序生成器，只生成与求值顺序无关的程序。作者用该生成器差分测试 OCaml 的两个编译器后端，并报告发现的多处编译器缺陷。
How does one test a language implementation with QuickCheck (aka. property-based testing)? One approach is to generate programs following the grammar of the language. But in a statically-typed language such as OCaml too many of these candidate programs will be rejected as ill-typed by the type checker. As a refinement Pałka et al. propose to generate programs in a goal-directed, bottom-up reading up of the typing relation. We have written such a generator. However many of the generated programs has output that depend on the evaluation order, which is commonly under-specified in languages such as OCaml, Scheme, C, C++, etc. In this paper we develop a type and effect system for conservatively detecting evaluation-order dependence and propose its goal-directed reading as a generator of programs that are independent of evaluation order. We illustrate the approach by generating programs to test OCaml's two compiler backends against each other and report on a number of bugs we have found doing so.
@article{MidtgaardJKNN17,
title = {Effect-driven QuickChecking of compilers},
author = {Jan Midtgaard and Mathias Nygaard Justesen and Patrick Kasting and Flemming Nielson and Hanne Riis Nielson},
journal = {Proceedings of the ACM on Programming Languages},
volume = {1},
number = {ICFP},
year = {2017},
doi = {10.1145/3110259}
}