一句话：提出高阶 MSL Horn 约束类并给出基于消解的判定过程，证明其与 HORS 模型检测可相互归约，并应用于高阶程序验证。
一元浅线性（MSL）是一阶 Horn 子句的可判定片段，自世纪之交被多次发现与再发现，广泛用于静态分析与验证。本文将其推广到高阶逻辑，提出高阶 MSL Horn 约束，并给出基于消解的判定过程。该约束类能够自然刻画高阶程序中复杂的调用与返回模式，因此非常适合高阶程序验证。作者进一步证明高阶 MSL 可满足性问题与 HORS 模型检测问题可相互归约，从而将高阶 MSL 视为高阶模型检测的一种基于约束的方法。最后，作者实现了该判定过程，并将其应用于经过验证的 socket 编程。
The monadic shallow linear (MSL) class is a decidable fragment of first-order Horn clauses that was discovered and rediscovered around the turn of the century, with applications in static analysis and verification. We propose a new class of higher-order Horn constraints which extend MSL to higher-order logic and develop a resolution-based decision procedure. Higher-order MSL Horn constraints can quite naturally capture the complex patterns of call and return that are possible in higher-order programs, which make them well suited to higher-order program verification. In fact, we show that the higher-order MSL satisfiability problem and the HORS model checking problem are interreducible, so that higher-order MSL can be seen as a constraint-based approach to higher-order model checking. Finally, we describe an implementation of our decision procedure and its application to verified socket programming.