Mon 16 Jan 2023 11:22 - 11:45 at Studio 1 - Logical Foundations Chair(s): Robbert Krebbers

A surprising result of Pitts (1992) says that propositional quantifiers are definable internally in intuitionistic propositional logic (IPC). The main contribution of this paper is to provide a formalization of Pitts’ result in the Coq proof assistant, and thus a verified implementation of Pitts’ construction. We in addition provide an OCaml program, extracted from the Coq formalization, which computes propositional formulas that realize intuitionistic versions of $\exists p \phi$ and $\forall p \phi$ from $p$ and $\phi$.

Mon 16 JanDisplayed time zone: Eastern Time (US & Canada) change

 11:00 - 12:30 Logical FoundationsCPP at Studio 1 Chair(s): Robbert Krebbers Radboud University Nijmegen 11:0022mTalk A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systemsdistinguished paperCPPChristina Kohl University of Innsbruck, Aart Middeldorp University of Innsbruck 11:2222mTalk Formalizing and computing propositional quantifiersremote presentationCPPHugo Férée Université Paris Cité / IRIF, Sam van Gool Université Paris Cité / IRIF 11:4522mTalk Encoding Dependently-Typed Constructions into Simple Type Theoryremote presentationCPPAnthony Bordg University of Cambridge, Adrián Doña Mateo The University of Edinburgh 12:0722mTalk A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl)CPPYannick Forster Inria, Felix Jahn Saarland University, Gert Smolka Saarland University