Hybrid realizability for intuitionistic and classical choice

DOI10.1145/2933575.2934511zbMATH Open1394.03021OpenAlexW2531070608MaRDI QIDQ4635918FDOQ4635918

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

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

Mathematics Subject Classification ID

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

Cited In (7)

• On bar recursion and choice in a classical setting
• Realizability of the axiom of choice in HOL. (An analysis of Krivine's work)
• Preservation of choice principles under realizability
• Title not available (Why is that?)
• A classical sequent calculus with dependent types
• Intuitionistic choice and restricted classical logic
• Typed realizability for first-order classical analysis

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)