Agda 中 System T 强规范化定理的形式化证明
计算机科学中的逻辑
2023-03-24 v1
摘要
我们提出了一个用于一阶语法下 lambda 演算形式化元理论的框架，具有两类名字，一类表示自由与约束变量，另一类表示常量，并使用 Stoughton 的多重替换。在该框架之上，我们形式化了 Girard 关于简单类型 lambda 演算和 System T 的强规范化定理的证明。对于后者，我们还给出了原始证明的一种简化。整个开发已使用 Agda 系统进行了机器检验。
引用
@article{arxiv.2303.13258,
title = {A Formal Proof of the Strong Normalization Theorem for System T in Agda},
author = {Sebastián Urciuoli},
journal= {arXiv preprint arXiv:2303.13258},
year = {2023}
}
备注
In Proceedings LSFA 2022, arXiv:2303.12680