Lambda-calcul, évaluation paresseuse et mise en mémoire
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 25 (1991) no. 1, pp. 67-84.
@article{ITA_1991__25_1_67_0,
     author = {Krivine, Jean-Louis},
     title = {Lambda-calcul, \'evaluation paresseuse et mise en m\'emoire},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     pages = {67--84},
     publisher = {EDP-Sciences},
     volume = {25},
     number = {1},
     year = {1991},
     zbl = {0717.03003},
     mrnumber = {1104412},
     language = {fr},
     url = {www.numdam.org/item/ITA_1991__25_1_67_0/}
}
Krivine, Jean-Louis. Lambda-calcul, évaluation paresseuse et mise en mémoire. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 25 (1991) no. 1, pp. 67-84. http://www.numdam.org/item/ITA_1991__25_1_67_0/

1. H. P. Barendregt, The lambda calculus, North Holland, 1984. | MR 774952 | Zbl 0551.03007

2. J. Y. Girard, Une extension de l'interprétation de Gödel à l'analyse, et son application à l'élimination des coupures, Proc. 2nd Scand. Logic Symp., 1970, North Holland, p. 63-92. | MR 409133 | Zbl 0221.02013

3. J. L. Krivine, Lambda-calcul typé, Masson, 1990. | MR 1162977

4. J. L. Krivine et M. Parigot, Programming with proofs, 6th Symp.. Comp. Theory 87, J. Inf. Process. Cybern., 3, 1990, p. 149-157. | MR 1056588 | Zbl 0699.68020

5. D. Leivant, Reasoning about Functional Programs and Complexity Classes Associated with Type Disciplines, 24th Symp. on Found. of Comp. Sci., 1983, p. 460-469.

6. M. Parigot, Programming with Proofs: a Second Order Type Theory, Proc. ESOP'88, Lect. Notes in Comp. Sci., 300, p. 145-159.

7. J. L. Krivine, Opérateurs de mise en mémoire et traduction de Gödel, Archiv for math. Logic (à paraître). | MR 1080590 | Zbl 0712.03009