使用合成受护卫域理论的渐近类型指称语义（扩展版）

渐近类型编程语言允许可靠地混合静态和动态类型编程风格，这给元理论学家带来了巨大挑战。即使是简单的可靠渐近类型语言也至少包含递归和错误，而现实的语言还包含内存位置的运行时分配和动态类型标签。此外，渐近类型语言所期望的元理论性质变得越来越复杂：基于类型的等式推理的有效性，以及被称为渐近性的关系性质。许多近期工作致力于验证这些性质，但由此产生的数学推导高度重复且繁琐，很少有可重用的定理能在不同推导中保留。在这项工作中，我们提出了一种使用受护卫域理论开发的渐近类型的新指称语义。受护卫域理论结合了步进索引逻辑关系在建模高级编程特性方面的通用性，以及指称语义的模块性和可重用性。我们用一个简单的渐近类型 lambda 演算模型证明了该方法的可行性，并证明了该指称模型的 beta-eta 等价有效性和渐近性定理。该模型应为渐近类型程序语义的可重用数学理论提供基础。最后，我们在 Guarded Cubical Agda（Agda 的一个近期扩展，支持我们使用的受护卫递归构造）中机械化证明了我们推导的大部分核心定理。