Opérateurs de mise en mémoire et traduction de Gödel. - Jean-Louis Krivine (Arch. Math. Log., 1990)

Programming with Proofs. - Jean-Louis Krivine; Michel Parigot (J. Inf. Process. Cybern., 1990)

Lambda-calcul, évaluation paresseuse et mise en mémoire. - Jean-Louis Krivine (RAIRO Theor. Informatics Appl., 1991)

Lambda-calculus, types and models. - Jean-Louis Krivine (Masson, 1993)

Classical Logic, Storage Operators and Second-Order lambda-Calculus. - Jean-Louis Krivine (Ann. Pure Appl. Log., 1994)

A General Storage Theorem for Integers in Call-by-Name lambda-Calculus. - Jean-Louis Krivine (Theor. Comput. Sci., 1994)

About Classical Logic and Imperative Programming. - Jean-Louis Krivine (Ann. Math. Artif. Intell., 1996)

Une preuve formelle et intuitionniste du théorème de complétude de la logique classique. - Jean-Louis Krivine (Bull. Symb. Log., 1996)

Disjunctive Tautologies as Synchronisation Schemes. - Vincent Danos; Jean-Louis Krivine (CSL, 2000)

The Curry-Howard Correspondence in Set Theory. - Jean-Louis Krivine (LICS, 2000)

Typed lambda-calculus in classical Zermelo-Frænkel set theory. - Jean-Louis Krivine (Arch. Math. Log., 2001)

Dependent choice, 'quote' and the clock. - Jean-Louis Krivine (Theor. Comput. Sci., 2003)

Valid formulas, games and network protocols - Jean-Louis Krivine; Yves Legrandgérard (CoRR, 2007)

A call-by-name lambda-calculus machine. - Jean-Louis Krivine (High. Order Symb. Comput., 2007)

Structures de réalisabilité, RAM et ultrafiltre sur N - Jean-Louis Krivine (CoRR, 2008)

Algèbres de réalisabilité: un programme pour bien ordonner R - Jean-Louis Krivine (CoRR, 2010)

Realizability algebras: a program to well order R - Jean-Louis Krivine (Log. Methods Comput. Sci., 2011)

Realizability algebras II : new models of ZF + DC - Jean-Louis Krivine (Log. Methods Comput. Sci., 2012)

On the Structure of Classical Realizability Models of ZF. - Jean-Louis Krivine (TYPES, 2014)

Bar recursion in classical realisability : dependent choice and well ordering of R. - Jean-Louis Krivine (CoRR, 2015)

Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis. - Jean-Louis Krivine (CSL, 2016)

Realizability algebras III: some examples. - Jean-Louis Krivine (Math. Struct. Comput. Sci., 2018)

A program for the full axiom of choice. - Jean-Louis Krivine (Log. Methods Comput. Sci., 2021)