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

We discuss and compare two Coq mechanisations of Sierpinski’s result that the generalised continuum hypothesis (GCH) implies the axiom of choice (AC). The first version shows the result, originally stated in first-order ZF set-theory, for a higher-order set theory convenient to work with in Coq. The second version presents a corresponding theorem for Coq’s type theory itself, concerning type-theoretic formulations of GCH and AC. Both versions rely on the classical law of excluded middle and extensionality assumptions but we localise the use of axioms where possible.

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