一句话：提出 weaning 翻译，首次在依赖类型论 CIC 中安全引入异常、非终止、非确定性等计算效应。
论文研究如何在依赖类型论中引入计算效应（如异常、非终止、非确定性、写操作）这一长期难题。作者指出，传统的单子翻译在存在类型依赖时会失效，并借助 call-by-push-value 分解说明其失败的根源：类型依赖于项，而效应会改变项的计算行为。为此他们提出 weaning 翻译，其关键条件是单子的代数宇宙自身必须构成一个代数。该翻译适用于带受限依赖消去的归纳构造演算（CIC），随后作者将参数化（parametricity）技术与 weaning 翻译相结合，把结果推广到完整 CIC，从而给出首个带效应的 CIC 版本。
We define a monadic translation of type theory, called the weaning translation, that allows for a large range of effects in dependent type theory-such as exceptions, non-termination, non-determinism or writing operations. Through the light of a call-by-push-value decomposition, we explain why the traditional approach fails with type dependency and justify our approach. Crucially, the construction requires that the universe of algebras of the monad forms itself an algebra. The weaning translation applies to a version of the Calculus of Inductive Constructions (CIC) with a restricted version of dependent elimination. Finally, we show how to recover a translation of full CIC by mixing parametricity techniques with the weaning translation. This provides the first effectful version of CIC.