Realizability of the Axiom of Choice in HOL. (An Analysis of Krivine's Work)

Issue title: Logic for Pragmatics

Article type: Research Article

Authors: Raffalli, Christophe | Ruyer, Frédéric

Affiliations: Laboratoire de Mathématique, Université de Savoie, 73376 Le Bourget-du-Lac cedex, France. E-mails: christophe.raffalli@univ-savoie.fr, frederic.ruyer@univ-savoie.fr

Note: [] Address for correspondence: Laboratoire de Mathématique, Université de Savoie, 73376 Le Bourget-du-Lac cedex, France

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.

Journal: Fundamenta Informaticae, vol. 84, no. 2, pp. 241-258, 2008