Write a Blog >>
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 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
Dominik KirstSaarland University, Felix RechSaarland University
Pre-print Media Attached
18:30 - 18:45
Talk
Formalizing Category Theory in Agda
CPP
Jason Z.S. HuMcGill University, Jacques CaretteMcMaster University
Pre-print Media Attached