caa a22 4500 465743714 CHVBK 20180323111814.0 cr unu---uuuuu 170327e19900701xx s 000 0 fre 10.1007/BF01792986 doi (NATIONALLICENCE)springer-10.1007/BF01792986 Krivine Jean-Louis Equipe de Logique mathématique, Université Paris VII, C.N.R.S., Tour 45-55, 5e étage, 2 place 2, place Jussieu, F-75251, Paris Cedex 05, France aut Opérateurs de mise en mémoire et traduction de Gödel [Elektronische Daten] [Jean-Louis Krivine] Inλ-calculus, the strategy of leftmost reduction ("call-by-name”) is known to have good mathematical properties; in particular, it always terminates when applied to a normalizable term. On the other hand, with this strategy, the argument of a function is re-evaluated at each time it is used. To avoid this drawback, we define the notion of "storage operator”, for each data type. IfT is a storage operator for integers, for example, let us replace the evaluation, by leftmost reduction, ofϕτ (whereτ is an integer, andϕ anyλ-term) by the evaluation oftτϕ. Then, this computation is the same as the following: first computeτ up to some reduced formτ 0, and then applyϕ toτ 0. So, we have simulated "call-by-value” evaluation within the strategy of leftmost reduction. The main theorem of the paper (Corollary of Theorem 4.1) shows that, in a second orderλ-calculus, using Gödel's translation of classical intuitionistic logic, we can find a very simple type (or specification) for storage operators. Thus, it gives a way to get such operators, which is to prove this type in second order intuitionistic predicate calculus. Springer-Verlag, 1990 Archive for Mathematical Logic Springer-Verlag 30/4(1990-07-01), 241-267 0933-5846 30:4<241 1990 30 153 https://doi.org/10.1007/BF01792986 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/BF01792986 text/html Onlinezugriff via DOI NATIONALLICENCE 100 1- Krivine Jean-Louis Equipe de Logique mathématique, Université Paris VII, C.N.R.S., Tour 45-55, 5e étage, 2 place 2, place Jussieu, F-75251, Paris Cedex 05, France aut NATIONALLICENCE 773 0- Archive for Mathematical Logic Springer-Verlag 30/4(1990-07-01), 241-267 0933-5846 30:4<241 1990 30 153 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer