一句话：研究 CIC 的渐进化，揭示渐进性与归一化、宇宙封闭的权衡，并给出三种折中方案及其元理论。
论文研究归纳构造演算（CIC）的渐进化，以支持不精确类型和项下的快速原型。作者用不可行定理揭示渐进性与 CIC 的归一化、宇宙对依赖积封闭之间的根本权衡（“渐进性火三角”），并提出参数化 GCIC，涵盖分别放松一条边的三种折中及其元理论。方法上，将 GCIC 双向精化为依赖类型转换演算 CastCIC，阐明类型、转换与渐进保证的关联；用 CastCIC 的语法模型设计安全合流归约，并在适用时建立归一化；再以语义模型研究静态/动态渐进保证及 New 和 Ahmed 的嵌入-投影对渐进性。该工作为可塑证明助手和依赖类型语言铺路。
We investigate gradual variations on the Calculus of Inductive Construction (CIC) for swifter prototyping with imprecise types and terms. We observe, with a no-go theorem, a crucial trade-off between graduality and the key properties of normalization and closure of universes under dependent product that CIC enjoys. Beyond this Fire Triangle of Graduality, we explore the gradualization of CIC with three different compromises, each relaxing one edge of the Fire Triangle. We develop a parametrized presentation of Gradual CIC (GCIC) that encompasses all three variations, and develop their metatheory. We first present a bidirectional elaboration of GCIC to a dependently-typed cast calculus, CastCIC, which elucidates the interrelation between typing, conversion, and the gradual guarantees. We use a syntactic model of CastCIC to inform the design of a safe, confluent reduction, and establish, when applicable, normalization. We study the static and dynamic gradual guarantees as well as the stronger notion of graduality with embedding-projection pairs formulated by New and Ahmed, using appropriate semantic model constructions. This work informs and paves the way towards the development of malleable proof assistants and dependently-typed programming languages.
@article{paperbot1619,
title = {Gradualizing the Calculus of Inductive Constructions},
author = {Meven Lennon-Bertrand and Kenji Maillard and Nicolas Tabareau and Éric Tanter},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {44},
number = {2},
year = {2022},
doi = {10.1145/3495528}
}