一句话：提出消耗与持久类型系统，无需求值即可精确预测带控制算子函数式程序到范式的步数与范式大小。
本文研究如何用类型系统精确刻画带控制算子的函数式程序的动态性质。这类程序可实现复杂的续延与回溯，其求值行为通常难以静态预测。作者为经典逻辑设计了消耗类型与持久类型，证明该类型系统能够捕获与动态行为相关的精确度量。具体而言，类型系统可以在不实际执行程序的情况下，给出程序求值至范式所需的步数，以及该范式的规模。该工作表明，类型系统不仅能保证程序良类型，还能作为静态资源分析与求值行为预测的工具，为经典逻辑下的控制算子程序提供精确的动态性质刻画。
We prove that type systems are able to capture exact measures related to dynamic properties of functional programs with control operators, which allow implementing intricate continuations and backtracking. Our type systems give the number of evaluation steps to normal form as well as the size of this normal form without any evaluation being needed.
DOI 原文 ·
@inproceedings{paperbot5504,
title = {Consuming and Persistent Types for Classical Logic},
author = {Delia Kesner and Pierre Vial},
booktitle = {LICS},
year = {2020},
doi = {10.1145/3373718.3394774}
}