activity
20142026
most citedA Flexible Proof Format for SAT Solver-Elaborator Communication

6 citations · 13 across the 9 of their papers we have counts for

collaborators
Showing 2026 · math.LOShow all

1 paper · 2 filters

math.LO2026

CIC + EM Con(ZF): the consistency of ZF in type theory with excluded middle and no choice

Mario Carneiro

The sets-as-trees interpretation of set theory in a dependent type theory with an impredicative universe of propositions validates Zermelo set theory, and it validates Replacement…