Paper Info
Title
Realizability of the Axiom of Choice in HOL. (An Analysis of Krivine's Work)
Abstract
This paper is an introduction to recent works in realizability, mainly Krivine's work to realize the dependent choice axiom. We also show how to improve programs extracted from classical proofs by distinguishing formulas with and without algorithmic contents.
Year
Venue
Keywords
2008
Fundam. Inform.
dependent choice axiom,recent work,distinguishing formula,classical proof,algorithmic content,axiom of choice
Field
DocType
Volume
Axiom of choice,Axiom schema,Discrete mathematics,Combinatorics,Zermelo–Fraenkel set theory,Urelement,Scott's trick,Constructive set theory,Realizability,Mathematics,Choice function
Journal
84
Issue
ISSN
Citations 
2
0169-2968
2
PageRank 
References 
Authors
0.52
11
2
Name
Order
Citations
PageRank
Christophe Raffalli1295.55
Frédéric Ruyer220.52