POPL 2021
Sun 17 - Fri 22 January 2021 Online
Sun 17 Jan 2021 18:00 - 18:15 at CPP - Logic, Set Theory, and Category Theory Chair(s): Yannick Forster

We investigate the possibility of formalizing quantifiers in proof theory while avoiding, as far as possible, the use of true binding structures, $\alpha$-equivalence or variable renamings. We propose a solution with two kinds of variables in terms and formulas, as originally done by Gentzen. In this way formulas are first-order structures, and we are able to avoid capture problems in substitutions. However at the level of proofs and proof manipulations, some binding structure seems unavoidable. We give a representation with de Bruijn indices for proof rules which does not impact the formula representation and keeps the whole set of definitions first-order.

#### Sun 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

 18:00 - 18:45 Logic, Set Theory, and Category TheoryCPP at CPP Chair(s): Yannick Forster Saarland UniversityStreamed session: https://youtu.be/U_ZT9hfDAUQ 18:0015mTalk An Anti-Locally-Nameless Approach to Formalizing QuantifiersCPP Olivier Laurent CNRS & ENS Lyon Pre-print Media Attached 18:1515mTalk The Generalised Continuum Hypothesis Implies the Axiom of Choice in CoqCPP Dominik Kirst Saarland University, Felix Rech Saarland University Pre-print Media Attached 18:3015mTalk Formalizing Category Theory in AgdaCPP Jason Z.S. Hu McGill University, Jacques Carette McMaster University Pre-print Media Attached