Jean-Louis Krivine

Equipe Preuves, Programmes et Systèmes

Université Paris 7, CNRS


tél : (33)1 57 27 92 39
fax : (33)1 57 27 92 97
krivine at pps dot jussieu dot fr


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 plus fréquemment, et les fontes sont plus lisibles.

Articles (sélection)

Bar recursion in classical realizability : dependent choice and continuum hypothesis (mise à jour 30/06/2016) Computer Science Logic 2016. arXiv.

On the structure of classical realizability models of ZF (mise à jour 19/05/2015) à paraître dans Proceedings TYPES'2014. arXiv.

Realizability algebras III : some examples (oct. 2012) (mise à jour 28/07/2015) Math. Struct. in Comp. Sc. - FirstView Article - May 2016, pp 1 - 32. arXiv

Realizability algebras II : new models of ZF + DC Log. Methods Comp. Sc. 8 (1:10) p. 1-28 (2012).

Realizability algebras : a program to well order R Log. Methods Comp. Sc. 7 (3:02) p. 1-47 (2011).

Valid formulas, games and network protocols (avec Y. arxivLegrandgé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.

Exposés (diapositives)

"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).

Textes divers

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)

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).

Livres

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)