Jean-Louis Krivine
Equipe Preuves, Programmes et Systèmes
Université Paris 7, CNRS
Université Paris 7 2 place Jussieu tél : (33)1 44 27 54 58 75251 Paris Cedex 05 fax : (33)1 44 27 61 48 FRANCE
Certains articles ou cours sont disponibles sur le serveur HAL du CNRS (référence HAL ou CEL). Toutefois, la version sur la présente page est mise à jour plus fréquemment.
Algèbres de réalisabilité : un programme pour bien ordonner R à paraître (2010). HAL (mise à jour : 3/03/2010)
Structures de réalisabilité, RAM et ultrafiltre sur N à paraître (2008) HAL.
Valid formulas, games and network protocols (avec Y. Legrandgérard) à paraître (2007). HAL version française HAL (mise à jour : 14/11/2007)
A propos de la chauve-souris et autres contes Notes de lecture (2008-2009)
Wigner, Curry et Howard Exposé au colloque de sciences cognitives ARCo'04, Compiègne (déc. 2004)
Realizability in classical logic Cours d'Ecole doctorale à l'Université de Marseille Luminy (mai 2004 ; dernière révision juil. 2005). A paraître dans Panoramas et synthèses, Société Mathématique de France. HAL.
A call-by-name lambda-calculus machine Higher Order and Symbolic Computation 20, p.199-207 (2007). HAL.
Dependent choice, `quote' and the clock Th. Comp. Sc., 308, p. 259-276 (2003). HAL.
Typed lambda-calculus in classical Zermelo-Fraenkel set theory Arch. Math. Log., 40, 3, p. 189-205 (2001).
Disjunctive tautologies and synchronisation schemes (avec V. Danos) Proceedings of CSL'2000, LNCS 1862, p. 292-301.
Ensembles et preuves Quadrature, 33, p. 9-16 (juillet 1998).
Une preuve formelle et intuitionniste du théorème de complétude de la logique classique Bull. Symb. Log. 2, 4, p. 405-421 (1996).
Un interpréteur du lambda-calcul (non publié).
Fonctions, programmes et démonstrations Gazette des mathématiciens (S.M.F.), 60, p. 63-73 (avril 1994).
Mathématiques des programmes et programme des mathématiques Turbulence, 1, p.94-100 (oct. 1994).
A general storage theorem for integers in call-by-name lambda-calculus Th. Comp. Sc., 129, p. 79-94 (1994).
Espaces de Banach stables (avec B. Maurey) Israël J. Math., 39, 4, p. 273-295 (1981).
Constantes de Grothendieck et fonctions de type positif sur les sphères Advances in Math., 31, p. 16-30 (1979).
Sous-espaces de dimension finie des espaces de Banach réticulés Annals of Math., 116, p. 1-29 (1976).
Langages à valeurs réelles et applications Fundamenta Mathematica, 81, p. 213-253 (1974).
Sous-espaces et cones convexes dans les espaces Lp Thèse d'Etat (1967).
Anneaux préordonnés Journal d'Analyse Math., 12, p. 307-326 (1964). HAL.
A program for the continuum hypothesis TLCA'09 (juillet 2009 - Brasilia, Brésil).
Realizability : a machine for Analysis and set theory Geocal'06 (février 2006 - Marseille, France); Mathlogaps'07 (juin 2007 - Aussois, France). CEL
The Curry-Howard correspondence in classical analysis and set theory WoLLIC'05 (juillet 2005 - Florianopolis, Brésil).
A machine for programs extracted with the axiom of choice APPSEM-II Workshop on the Krivine and ZINC abstract machines (mai 2005 - Birmingham, UK).
Realizing the axiom of dependent choice Workshop on Proof theory and algorithms (mars 2003 - Edinburgh, UK).
Two talks on specification and objects Spring school on Semantics of programming languages (2002 - Agay, France).
Realizability and forcing Logic Colloquium (2000 - Paris, France).
Lambda-calculus, types and models Ellis Horwood (1993) (dernière mise à jour : 22/01/2009)
Théorie des ensembles. Cassini, Paris; 1ère édition (1998), 2ème édition (2007)
Lambda-calcul, types et modèles. Masson (1990)
Eléments de logique mathématique (théorie des modèles) (avec G. Kreisel) Dunod (1966)
Elements of mathematical logic (model theory) (with G. Kreisel) North Holland (1967)