milan米兰体育 用类型理论编码 Z 样式模式

引用

Maharaj S (1994) 在类型理论中编码 Z 样式模式。见：Barendregt H 和 Nipkow T（编辑）证明和程序的类型：国际研讨会 TYPES'93，荷兰奈梅亨，1993 年 5 月 24 日至 28 日 论文选集。计算机科学讲义，806。国际研讨会 TYPES'93，荷兰奈梅亨，1993 年 5 月 24 日至 1993 年 5 月 28 日。柏林海德堡：Springer，第 238-262 页。 http://link.springer.com/chapter/10.1007/3-540-58085-9_79#； https://doi.org/10.1007/3-540-58085-9_79

摘要
Z 规范语言的一个显着特征是其模式演算，它允许将规范打包并组合在一起形成新的规范。我们研究将模式演算转换为类型论 UTT 的方法。我们首先尝试将模式直接编码为 Σ 类型。事实证明这并不令人满意，因为对模式演算的操作进行编码需要能够对模式语法执行计算，因此我们开发了也表示该语法的方法。这些方法也依赖于 Σ 类型，但以非常规方式使用它们。我们定义了模式实现的概念，并使用乐高证明检查器来证明有关实现和 Z 模式微积分运算编码之间相互作用的一些定理。