Hybrid realizability for intuitionistic and classical choice

DOI10.1145/2933575.2934511MaRDI QIDQ4635918zbMATH OpenOpenAlexFDO

Authors Valentin Blot

Publication date 23 April 2018

Published in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2933575.2934511

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40) Axiom of choice and related propositions (03E25) First-order arithmetic and fragments (03F30)

Recommendations

• scientific article; zbMATH DE number 5851813
• scientific article; zbMATH DE number 2185652
• On bar recursion and choice in a classical setting
• A Constructive Proof of Dependent Choice, Compatible with Classical Logic
• On the computational content of the axiom of choice

Cited in

(10)

• Intuitionistic choice and restricted classical logic
• On bar recursion and choice in a classical setting
• A classical sequent calculus with dependent types
• scientific article; zbMATH DE number 2185652 (Why is no real title available?)
• Typed realizability for first-order classical analysis
• Realizability of the axiom of choice in HOL. (An analysis of Krivine's work)
• On the computational content of the axiom of choice
• scientific article; zbMATH DE number 1497731 (Why is no real title available?)
• A program for the full axiom of choice
• Preservation of choice principles under realizability

This page was built for publication: Hybrid realizability for intuitionistic and classical choice

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635918)