一句话：提出基于精化类型的可视化合成范式，并用轻量级双向类型检查剪枝，显著加速生成数据变换与可视化程序。
可视化在数据探索、验证与分享洞察中至关重要。本文提出基于精化类型的可视化合成新范式：除输入输出示例外，用户可用精化类型注解约束示例可视化中的有效值范围，或表达不同可视化组件间的复杂交互。系统输出同时包含数据变换程序和可视化程序，且保证符合精化类型规约。为缓解合成过程的可扩展性挑战，作者引入一种利用轻量级双向类型检查来剪枝搜索空间的合成算法。实验表明，与先前工作相比，该算法带来显著加速。
Visualizations have become crucial in the contemporary data-driven world as they aid in exploring, verifying, and sharing insights obtained from data. In this paper, we propose a new paradigm of visualization synthesis based on refinement types. Besides input-output examples, users can optionally use refinement-type annotations to constrain the range of valid values in the example visualization or to express complex interactions between different visual components. Our system's outputs include both data transformation and visualization programs that are consistent with refinement-type specifications. To mitigate the scalability challenge during the synthesis process, we introduce a new visualization synthesis algorithm that uses lightweight bidirectional type checking to prune the search space. As we demonstrate experimentally, this new synthesis algorithm results in significant speed-up compared to prior work.