POPL 2021 (series) / CPP 2021 (series) / Certified Programs and Proofs /
An Anti-Locally-Nameless Approach to Formalizing Quantifiers
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
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 University Streamed session: https://youtu.be/U_ZT9hfDAUQ | |||
18:00 - 18:15 Talk | An Anti-Locally-Nameless Approach to Formalizing Quantifiers CPP Olivier LaurentCNRS & ENS Lyon Pre-print Media Attached | ||
18:15 - 18:30 Talk | The Generalised Continuum Hypothesis Implies the Axiom of Choice in Coq CPP Pre-print Media Attached | ||
18:30 - 18:45 Talk | Formalizing Category Theory in Agda CPP Pre-print Media Attached |