我读过这篇论文 http://www21.in.tum.de/~berghofe/papers/TYPES2002_slides.pdf。
它包含第 7 页上的 Isabelle 类型系统的微积分。在这个微积分中，“术语有类型”和“证明有术语”。
1）关于这个微积分是否存在更详细的论文？
2）我不明白的唯一两个规则是与常量有关的规则。
2.1) “c_{[\vec{\tau}_n / \vec{\alpha}_n]}”是什么意思？它是一个常数的证明。例如，我们在第 9 页有常量“impI”。这些 tau 和 alpha 如何与“impI 的术语”相关联。
2.2)能否请您澄清一下规则 $\Sigma(c) [\vec{\tau}_n / \vec{\alpha}_n] $。?
乍一看，它可能被翻译为“任何依赖于证明（！）常量的任何一组术语，具有任意数量的类型而不是原子类型”，但我认为它没有任何意义。
3）我也对关于这种微积分的语义和/或它的正确性定理的论文感兴趣。
我感谢任何相关信息。谢谢！