×
Nour, Karim

Storage operators and \(\forall\)-positive types. (Opérateurs de mise en mémoire et types \(\forall\)-positifs.) (French) Zbl 0869.03009

RAIRO, Inform. Théor. Appl. 30, No. 3, 261-293 (1996).
In 1990, J.-L. Krivine introduced the notion of storage operator to simulate the “call by value” in a context of “call by name”. He has shown that, using Gödel’s translation from classical to intuitionistic logic, we can find a very simple type of AF2 type system for the storage operators [see J.-L. Krivine, Arch. Math. Logic 30, No. 4, 241-267 (1990; Zbl 0712.03009)]. In this paper, we study the \(\forall\)-positive types (the universal second-order quantifier appears positively in the types) and the Gödel transformations (a generalization of classical Gödel translation) of the system AF2. We generalize, by using a purely syntactic method, J.-L. Krivine’s theorem about these types and for these transformations.
Reviewer: K.Nour (Le Bourget du Lac)

Cited in 5 Documents

MSC:

03B40 Combinatory logic and lambda calculus

Keywords:

storage operator; AF2 type system; \(\forall\)-positive types; Gödel transformations; Gödel translation

Citations:

Zbl 0712.03009
PDF BibTeX XML Cite
\textit{K. Nour}, RAIRO, Inform. Théor. Appl. 30, No. 3, 261--293 (1996; Zbl 0869.03009)
Full Text: DOI EuDML

References:

[1] 1. H. BARENDREGT, The lambda calculus: Its Syntax and Semantics, North Holland, 1984. Zbl0551.03007 MR774952 · Zbl 0551.03007
[2] 2. J. Y. GIRARD, Y. LAFONT et P. TAYLOR, Proofs and types, Cambridge University Press, 1986. Zbl0671.68002 MR1003608 · Zbl 0671.68002
[3] 3. P. GIANNINI et S. RONCHI DELLA ROCCA. Characterization of typing in polymorphic type discipline. LICS, Edimbourg, 1988, p. 61-70.
[4] 4. J.-L. KRIVINE, Lambda calcul, évaluation paresseuse et mise en mémoire, Informatique Théorique et Application, 1991, 25, 1, p. 67-84. Zbl0717.03003 MR1104412 · Zbl 0717.03003
[5] 5. J.-L. KRIVINE, Lambda calcul, types et modèle, Masson, Paris, 1990. Zbl0697.03004 MR1162977 · Zbl 0697.03004
[6] 6. J.-L. KRIVINE, Opérateurs de mise en mémoire et traduction de Gödel, Archive for Mathematical Logic, 1990, 30, p. 241-267. Zbl0712.03009 MR1080590 · Zbl 0712.03009
[7] 7. J.-L. KRIVINE, Mise en mémoire (preuve générale). Manuscrit, 1991.
[8] 8. R. LABIB-SAMI. Typer avec (ou sans) types auxilières, Manuscrit, 1986.
[9] 9. K. NOUR, Opérateurs de mise en mémoire en lambda-calcul pur et typé, Thèse de doctorat, Université de Savoie, 1993.
[10] 10. K. NOUR, Opérateurs propres de mise en mémoire, C. R. Acad. Sci., 1993, 317, Série I, p. 1-6. Zbl0788.03015 MR1228953 · Zbl 0788.03015
[11] 11. K. NOUR, Strong storage operators and data types, Archive for Mathematical Logic, 1995 34, p. 65-78. Zbl0818.03004 MR1326890 · Zbl 0818.03004
[12] 12. K. NOUR, Preuve syntaxique d’un théorème de J.-L. Krivine sur les opérateurs de mise en mémoire, C. R. Acad. Sci., 1994, 318, Série I, p. 201-204. Zbl0792.03010 MR1262895 · Zbl 0792.03010
[13] 13. K. NOUR et R. DAVID, Storage operators and directed lambda-calculus, Journal of Symbolic Logic, 1995, 60, n^\circ 4, p. 1054-1086. Zbl0852.03007 MR1367196 · Zbl 0852.03007
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.