2010/02/18 by Jean-Louis Krivine, Krivine, Jean-Louis
Computer Science · Mathematics · #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.LO #math.LO
paper · pdf · doi:10.48550/arxiv.1002.3438
45 pages
openalex publication_date 2010/02/18 · arxiv created 2010/05/31 · arxiv updated 2010/06/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We give a method to transform into programs, classical proofs using a well ordering of the reals. The technics uses a generalization of Cohen's forcing and the theory of classical realizability introduced by the author.