OPÉRATEURS DE MISE EN MÉMOIRE ET TYPES any-POSITIFS

摘要

En 1990, J.-L. Krivine a introduit la notion d'opérateurs de mise en mémoire pour simuler « l'appel par valeur » dans le cadre de « l'appel par nom ». J. -L. Krivine a démontré qu'en utilisant la traduction de Goedel de la logique classique en logique intuitionniste, on peut trouver un type très simple du système AF2 pour les opérateurs de mise en mémoire. Dans cet article nous étudions les types any-positifs (le quantificateur universel du second ordre apparaît positivement dans les types), et les transformations de Goedel (une généralisation de la traduction de Goedel classique) du système AF2. Nous généralisons, en utilisant des méthodes purement syntaxiques, le théorème de J.-L. Krivine sur ces types et pour ces transformations.%In 1990, J.-L. Krivine introduced the notion of storage operator to simulate the "call by value" in a context of a "call by name". J.-L. Krivine has shown that using Goedel translation from classical to intuitionistic logic, we can find a very simple type of Afl type system for the storage operators. In this paper we study the any-positive types (the universel second order quantifier appears positively in the types), and the Goedel transformations (a generalization of classical Goedel translation) of the system AF2. We generalize, by using a pure syntaxic methods, the J. -L. Krivine theorem about these types and for these transformations.