Storage operators and forall-positive types of system TTR

TL;DR

This paper explores the properties of storage operators within the TTR type system, focusing on forall-positive types and G"odel transformations, extending Krivine's foundational work on call-by-value simulation.

Contribution

It generalizes Krivine's theorem to forall-positive types and G"odel transformations in the TTR system using syntactical methods, including the case of recursive integers.

Findings

Generalization of Krivine's theorem to TTR system

Proof of properties for recursive integers type

Extension of G"odel transformations in type analysis

Abstract

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\"odel 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\"odel transformations (a generalization of classical G\"odel 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.