一句话：提出单子仿射大小类型系统，可类型化概率高阶程序并证明其几乎必然终止。
本文研究概率高阶程序的几乎必然终止性，目标是在不牺牲可靠性的前提下超越普通强规范化。作者提出单子仿射大小类型（monadic affine sized types），它推广了通常的大小类型，引入更定量的类型信息，并施加仿射约束以保持证明可行。该类型系统足以类型化随机游走等经典概率终止程序。可类型化程序被证明几乎必然终止，证明基于可归约性（reducibility）方法，但需要对这一技术作出实质性适配。
We introduce a system of monadic affine sized types, which substantially generalizes usual sized types and allows in this way to capture probabilistic higher-order programs that terminate almost surely. Going beyond plain, strong normalization without losing soundness turns out to be a hard task, which cannot be accomplished without a richer, quantitative notion of types, but also without imposing some affinity constraints. The proposed type system is powerful enough to type classic examples of probabilistically terminating programs such as random walks. The way typable programs are proved to be almost surely terminating is based on reducibility but requires a substantial adaptation of the technique.
@article{paperbot713,
title = {Probabilistic Termination by Monadic Affine Sized Typing},
author = {Ugo Dal Lago and Charles Grellois},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {41},
number = {2},
year = {2019},
doi = {10.1145/3293605}
}