2026-07-22T08:26:57Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:17470 2024-03-06T11:00:03Z ddc:004 open_access

Proofs and Refutations for Intuitionistic and Second-Order Logic Barenbaum, Pablo Freund, Teodoro lambda-calculus propositions-as-types classical logic proof normalization The λ^{PRK}-calculus is a typed λ-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 λ^{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 λ^{PRK}, and we study canonicity results. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Pablo Barenbaum and Teodoro Freund 2023 Is Part Of LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2023.9 urn:nbn:de:0030-drops-174707 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.9 eng https://creativecommons.org/licenses/by/4.0/legalcode