论文标题
直觉和二阶逻辑的证明和反驳（扩展版本）
Proofs and Refutations for Intuitionistic and Second-Order Logic (Extended Version)
论文作者
论文摘要
lambda-prk-calculus是一种打字的lambda-calculus，可利用证明概念和反驳之间的双重性为经典命题逻辑提供了计算解释。在这项工作中，我们通过合并参数多态性和存在类型来扩展Lambda-prk以包含经典的二阶逻辑。该系统被证明具有良好的计算属性，例如类型保存，汇合和强范围，这是通过降低性参数确定的。我们确定了对二阶lambda-prk的直觉片段的证明的句法限制，我们研究了典型性结果。
The lambda-PRK-calculus is a typed lambda-calculus that exploits the duality between the notions of proof and refutation to provide a computational interpretation for classical propositional logic. In this work, we extend lambda-PRK to encompass classical second-order logic, by incorporating parametric polymorphism and existential types. The system is shown to enjoy good computational properties, such as type preservation, confluence, and strong normalization, which is established by means of a reducibility argument. We identify a syntactic restriction on proofs that characterizes exactly the intuitionistic fragment of second-order lambda-PRK, and we study canonicity results.
