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 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

 18:00 - 18:45: Logic, Set Theory, and Category TheoryCPP at CPP Chair(s): Yannick ForsterSaarland UniversityStreamed session: https://youtu.be/U_ZT9hfDAUQ 18:00 - 18:15Talk An Anti-Locally-Nameless Approach to Formalizing QuantifiersCPP Olivier LaurentCNRS & ENS Lyon Pre-print Media Attached 18:15 - 18:30Talk The Generalised Continuum Hypothesis Implies the Axiom of Choice in CoqCPP Dominik KirstSaarland University, Felix RechSaarland University Pre-print Media Attached 18:30 - 18:45Talk Formalizing Category Theory in AgdaCPP Jason Z.S. HuMcGill University, Jacques CaretteMcMaster University Pre-print Media Attached