Gradualizing the Calculus of Inductive Constructions
Gradualizing the Calculus of Inductive Constructions
复制标题
DOI：
10.1145/3495528
复制
发表时间：
2022-01-01
影响因子：
1.3
通讯作者：
Tanter，Eric
中科院分区：
文献类型：
--
作者：
Lennon-Bertrand，Meven;Maillard，Kenji;Tanter，Eric
我们研究了归纳构造演算(CIC)的渐变，以用于具有不精确的类型和术语的更快的原型制作。我们用一个不去定理观察到，在渐进性和CIC所享有的依赖积下宇宙的正规化和闭合的关键性质之间，存在着一个关键的权衡。在这个渐变的火三角之外，我们用三种不同的妥协来探索CIC的渐变，每个妥协都放松了火三角的一条边。我们开发了一个包含所有三种变体的渐进式CIC的参数表示(GCIC)，并发展了它们的元理论。我们首先从GCIC到依赖类型的CAST演算CastCIC的双向阐述，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.