一句话：将动态切片与 Galois 连接扩展到含引用和异常的命令式函数式程序，并证明其正确性与最优性。
程序切片可解释输出如何由输入产生。已有工作针对纯高阶函数式程序，将动态切片定义为部分输入格与部分输出格之间的 Galois 连接。本文把该框架扩展到命令式函数式程序，统一处理高阶函数、引用与异常。作者给出语义定义，并证明切片相对于求值轨迹的正确性与最优性；还实现原型工具并进行实验评估，表明该扩展可实际生成解释程序行为的切片。
Program slicing provides explanations that illustrate how program outputs were produced from inputs. We build on an approach introduced in prior work, where dynamic slicing was defined for pure higher-order functional programs as a Galois connection between lattices of partial inputs and partial outputs. We extend this approach to imperative functional programs that combine higher-order programming with references and exceptions. We present proofs of correctness and optimality of our approach and a proof-of-concept implementation and experimental evaluation.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{RicciottiSPC17,
title = {Imperative functional programs that explain their work},
author = {Wilmer Ricciotti and Jan Stolarek and Roly Perera and James Cheney},
journal = {Proceedings of the ACM on Programming Languages},
volume = {1},
number = {ICFP},
year = {2017},
doi = {10.1145/3110258}
}