1 Search Results for "Freund, Teodoro"

Document
DOI: 10.4230/LIPIcs.CSL.2023.9
Proofs and Refutations for Intuitionistic and Second-Order Logic

Authors: Pablo Barenbaum and Teodoro Freund

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
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.
Cite as

Pablo Barenbaum and Teodoro Freund. Proofs and Refutations for Intuitionistic and Second-Order Logic. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{barenbaum_et_al:LIPIcs.CSL.2023.9,
  author =	{Barenbaum, Pablo and Freund, Teodoro},
  title =	{{Proofs and Refutations for Intuitionistic and Second-Order Logic}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{9:1--9:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.9},
  URN =		{urn:nbn:de:0030-drops-174707},
  doi =		{10.4230/LIPIcs.CSL.2023.9},
  annote =	{Keywords: lambda-calculus, propositions-as-types, classical logic, proof normalization}
}
  • Refine by Author
  • 1 Barenbaum, Pablo
  • 1 Freund, Teodoro

  • Refine by Classification
  • 1 Theory of computation → Proof theory
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 1 classical logic
  • 1 lambda-calculus
  • 1 proof normalization
  • 1 propositions-as-types

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2023

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact