Opérateurs de mise en mémoire et traduction de Gödel
作者： Jean-Louis Krivine
DOI: 10.1007/BF01792986
关键词:
摘要: Enλ-calcul, la strategie de reduction a gauche (appel par nom) a, comme on sait, bonnes proprietes mathematiques; en particulier, elle termine toujours si l'applique un terme normalisable. Mais, avec cette strategie, l'argument d'une fonction est recalcule chaque utilisation.
springer.com
philpapers.org
sci-hub.se 参考文章(5)
Jean-Louis Krivine, Lambda-calcul, évaluation paresseuse et mise en mémoire Theoretical Informatics and Applications. ,vol. 25, pp. 67- 84 ,(1991) , 10.1051/ITA/1991250100671
Daniel Leivant, Reasoning about functional programs and complexity classes associated with type disciplines 24th Annual Symposium on Foundations of Computer Science (sfcs 1983). pp. 460- 469 ,(1983) , 10.1109/SFCS.1983.50
Jean-Louis Krivine, Lambda-calcul : types et modèles Masson. ,(1990)
Jean-Yves Girard, Une Extension De ĽInterpretation De Gödel a ĽAnalyse, Et Son Application a ĽElimination Des Coupures Dans ĽAnalyse Et La Theorie Des Types Proceedings of the Second Scandinavian Logic Symposium. ,vol. 63, pp. 63- 92 ,(1971) , 10.1016/S0049-237X(08)70843-7
Harold Hodes, H. P. Barendregt, The | lambda-Calculus. The Philosophical Review. ,vol. 97, pp. 132- ,(1988) , 10.2307/2185110