Realizability of the axiom of choice in HOL. (An analysis of Krivine's work)

zbMATH Open1183.03009MaRDI QIDQ3532208FDOQ3532208

Authors: Frédéric Ruyer, Christophe Raffalli 

Publication date: 3 November 2008

Recommendations

• Dependent choice, `quote' and the clock
• scientific article; zbMATH DE number 5360217
• scientific article; zbMATH DE number 2185652
• Hybrid realizability for intuitionistic and classical choice
• scientific article; zbMATH DE number 1497731

zbMATH Keywords

realizabilityaxiom of choicehigher-order logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Axiom of choice and related propositions (03E25)

Cited In (2)

• A realizability interpretation of Church's simple theory of types
• Variations on realizability: realizing the propositional axiom of choice

This page was built for publication: Realizability of the axiom of choice in HOL. (An analysis of Krivine's work)

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