Jean-Louis Krivine
Equipe I.R.I.F. (P.P.S.)
Université de Paris-Cité, CNRS
tél : (33)1 57 27 92 39 fax : (33)1 57 27 92 97
Certains articles ou cours sont disponibles sur les serveurs HAL et CEL (CNRS) ou arXiv. Toutefois, leur version sur la présente page est remise à jour, et les fontes sont plus lisibles.
A program for the full axiom of choice Log. Met. Comp. Sc. Volume 17, Issue 3, pp. 21:1–21:22, Sept. 2021. arXiv
Realizability algebras III : some examples Math. Struct. in Comp. Sc. - Volume 28, Issue 1, pp. 45-76 (2018). arXiv
Bar recursion in classical realizability : dependent choice and continuum hypothesis Proceedings CSL 2016, LIPIcs vol. 62 (2016) pp. 25:1-25:11. arXiv.
On the structure of classical realizability models of ZF Proc. TYPES'2014 - LIPIcs vol. 39 (2015) p. 146-161. arXiv.
Realizability algebras II : new models of ZF + DC Log. Met. Comp. Sc. 8 (1:10) p. 1-28 (2012).
Realizability algebras : a program to well order R Log. Met. Comp. Sc. 7 (3:02) p. 1-47 (2011).
Valid formulas, games and network protocols (avec Y. Legrandgérard) (2007) HAL Version française HAL
Realizability in classical logic Cours d'Ecole doctorale à l'Université de Marseille Luminy (mai 2004).
In Interactive models of computation and program behaviour. Panoramas et synthèses, Société
Mathématique de France, 27, p. 197-229 (2009). 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.
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é).
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).
Modèles de ZF + AC dans lesquels tout ensemble de réels définissable en termes d'ordinaux est mesurable-Lebesgue C. R. Acad. Sc. Paris, série A, t. 269, p. 549-552 (1969).
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.
New realizability models (at last a program for AC) Realizability workshop 2019 - CIRM - Marseille.
Curry-Howard et choix dépendant Journées P.P.S. 2018 - Paris.
A propos des modèles de réalisabilité de ZF Colloque Réalisabilité, juin 2018 - CIRM - Marseille.
Bar recursion in classical realizability : dependent choice and continuum hypothesis CSL août 2016 - Marseille.
"Bar recursion”, sémantique dénotationnelle et réalisabilité classique Séminaire, mars 2015 - Marseille.
50 years after forcing, the Curry-Howard correspondence gives new models of ZF Institut Henri Poincaré, avril 2014 - Paris.
Some properties of realizability models Workshop on realizability (juin 2012 - Chambéry, France).
New models of ZF Workshop on proof theory (novembre 2010 - Münchenwiler, Suisse) (mise à jour 21 novembre 2011).
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).
Realizability and forcing Logic Colloquium (2000 - Paris, France).
A propos de l'intuition en mathématiques (mars 2018).
A propos de la théorie des démonstrations Colloque en l'honneur de René Cori (sept. 2014).
Du programme de Hilbert aux programmes informatiques Leçons de mathématiques d'aujourd'hui, Bordeaux (janv. 2012)
A propos de la chauve-souris et autres contes (décembre 2008)
Tiers exclu et choix dépendant Colloque en l'honneur de Daniel Lacombe (IHP octobre 2005)
Wigner, Curry et Howard Exposé au colloque de sciences cognitives ARCo'04, Compiègne (déc. 2004)
Ensembles et preuves Quadrature, 33, p. 9-16 (juillet 1998).
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).
Les décompilateurs (l'Univers en tête). Calvage et Mounet (2024)
Lambda-calculus, types and models Ellis Horwood (1993) (mise à jour 3 novembre 2011) CEL
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)