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
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 remise à jour plus fréquemment.
Realizability algebras II : new models of ZF + DC Logical Methods in Computer Science 8 (1:10) p. 1-28 (2012).
Realizability algebras : a program to well order R Logical Methods in Computer Science 7 (3:02) p. 1-47 (2011).
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
Wigner, Curry et Howard Exposé au colloque de sciences cognitives ARCo'04, Compiègne (décembre 2004)
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.
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 (octobre 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.
New models of ZF Workshop on proof theory (novembre 2010 - Münchenwiler, Suisse) (mise à jour 21 novembre 2011).
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) (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)