A Constructive Proof of Dependent Choice, Compatible with Classical Logic

DOI10.1109/LICS.2012.47zbMath1364.03070OpenAlexW2068413129MaRDI QIDQ2986812

Hugo Herbelin

Publication date: 16 May 2017

Published in: 2012 27th Annual IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1109/lics.2012.47

zbMATH Keywords

constructive logicclassical logicdependent choicestrong existential elimination

Mathematics Subject Classification ID

Axiom of choice and related propositions (03E25)

Related Items (7)

Completeness and decidability results for CTL in constructive type theory ⋮ The effects of effects on constructivism ⋮ ANF preserves dependent types up to extensional equality ⋮ Stateful Realizers for Nonstandard Analysis ⋮ Adding Negation to Lambda Mu ⋮ Delimited control operators prove double-negation shift ⋮ A Classical Sequent Calculus with Dependent Types

This page was built for publication: A Constructive Proof of Dependent Choice, Compatible with Classical Logic