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

• Autorzy: Raffalli C. , Ruyer F.
• Języki publikacji: EN

Abstrakty

EN

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.

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 84, nr 2
• Strony: 241--258
• Opis fizyczny: bibliogr. 16 poz.

Twórcy

autor

Raffalli C.

autor

Ruyer F.

• Laboratoire de Mathematique, Universite de Savoie F-73376 Le Bourget du Lac., France,

Bibliografia

• [1] Berardi, S.: Pruning simply typed _-terms, Journal of Logic and Computation, 6, 1996, 663-681.
• [2] Church, A.: A formulation of the simple theory of types, Journal of Symbolic Logic, 5, 1940, 56-80.
• [3] Coquand, T.: A semantics of evidence for classical arithmetic, Journal of Symbolic Logic, 60, 1995, 325-337.
• [4] Curmin, P.: Marquage des preuves et extraction de programmes, Ph.D. Thesis, ´Equipe de logique Université Paris VII, 1999.
• [5] Farkh, S., Nour, K.: Complete types in an extension of the system AF2, Journal of Applied Non-Classical Logics, 13, 2003, 73-85.
• [6] Hayashi, S.: Can Poofs be Animated by Games?, TLCA, 2005.
• [7] Krivine, J.: Dependent choice, "quote" and the clock, Th. Comp. Sc., 308, 2003, 259-276.
• [8] Krivine, J.: Realizability in classical logic, 2004, Phd Course, To appear in Panoramas et synth`eses, Société Mathématique de France.
• [9] Krivine, J., Parigot, M.: Programming with Proofs, Inf. Process. Cybern., EIK 26(3), 1990, 149-167.
• [10] Parent, C.: Synthesizing proofs from programs in the Calculus of Inductive Constructions, Mathematics for Programs Constructions, 947, Springer Verlag, 1995.
• [11] Parigot, M.: Recursive programming with proofs, Theoretical Computer Science, 94, 1992, 335-356.
• [12] Paulin-Mohring, C., Werner, B.: Synthesis of ML programs in the system Coq, Journal of Symbolic Computation, 15, 1993, 607-640.
• [13] Raffalli, C.: System ST, Toward A Type System for Extraction AND Proof of Programs, Archive for Pure and Applied Logic, 122, 2002, 107-130.
• [14] Raffalli, C.: "The PhoX proof assistant version 0.8", 2002, Software available on the Internet: http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html.
• [15] Raffalli, C.: System ST, _-reduction and completeness, Logic In Computer Science, "IEEE", Toronto, 2003.
• [16] Ruyer, F.: Types, sous-types et preuves, Ph.D. Thesis, Universit´e de Savoie, 2006.