Storage operators and forall-positive types of system TTR
Nour, Karim
HAL, hal-00381043 / Harvested from HAL
In 1990, J.L. Krivine introduced the notion of storage operator to simulate "call by value" in the "call by name" strategy. J.L. Krivine has shown that, using Gödel translation of classical into intuitionitic logic, we can find a simple type for the storage operators in AF2 type system. This paper studies the $\forall$-positive types (the universal second order quantifier appears positively in these types), and the Gödel transformations (a generalization of classical Gödel translation) of TTR type system. We generalize, by using syntaxical methods, the J.L. Krivine's Theorem about these types and for these transformations. We give a proof of this result in the case of the type of recursive integers.
Publié le : 1996-07-05
Classification:  [MATH.MATH-LO]Mathematics [math]/Logic [math.LO]
@article{hal-00381043,
     author = {Nour, Karim},
     title = {Storage operators and forall-positive types of system TTR},
     journal = {HAL},
     volume = {1996},
     number = {0},
     year = {1996},
     language = {en},
     url = {http://dml.mathdoc.fr/item/hal-00381043}
}
Nour, Karim. Storage operators and forall-positive types of system TTR. HAL, Tome 1996 (1996) no. 0, . http://gdmltest.u-ga.fr/item/hal-00381043/