## A semantical storage operator theorem for all types.(English)Zbl 0899.03014

The notion of storage operator was introduced by J.-L. Krivine to simulate, for a given set of terms, “call by value” in a “call by name”. The storage operator theorem is valid for a type $$D$$ if any term of type $$\neg D\to\neg D^*$$ is a storage operator for the elements of $$D$$ ($$D^*$$ being the Gödel translation of $$D$$). Krivine proved the storage operator theorem for the type of integer in the AF2 type system. This result has been extended to any type with only positive $$\forall$$-quantifiers by Krivine, using a semantical proof, and by Nour (using a syntactic proof). The author gives a new notion of semantical storage operator which is equivalent to Krivine and Nour’s notion for data-types. Its new storage operator theorem gives a sufficient condition to ensure the existence of semantical storage operators for an arbitrary type. The proof technique is a simplification of Krivine’s techniques using only 2 variables (while Nour uses the directed $$\lambda$$-calculus).

### MSC:

 03B40 Combinatory logic and lambda calculus 68Q60 Specification and verification (program logics, model checking, etc.) 03F35 Second- and higher-order arithmetic and fragments
Full Text:

### References:

  Barendregt, H. P., The Lambda Calculus: its Syntax and Semantics (1984), North-Holland: North-Holland Amsterdam · Zbl 0551.03007  Krivine, J.-L., Opérateurs de mise en mémoire et traduction de Godël, (Equipe de Logique de Paris 7. Equipe de Logique de Paris 7, Technical Report, 3 (December 1989)) · Zbl 0712.03009  Krivine, J.-L., Opérateurs de mise en mémoire et traduction de gödel, Arch. Math. Logic, 30, 241-267 (1990) · Zbl 0712.03009  Krivine, J.-L., Lambda-Calculus: Types and Models, Computers and their Applications (1993), Ellis Horwood: Ellis Horwood Chichester · Zbl 0779.03005  Krivine, J.-L., Mise en mémoire, preuve général (1993), manuscript  Krivine, J.-L., Classical logic, storage operators and second order λ-calculus, Ann. Pure Appl. Logic, 68, 53-78 (1994) · Zbl 0814.03009  Krivine, J.-L.; Parigot, M., Programming with proofs, Inform. Process. Cybernet., EIK-26, 3, 149-167 (1990) · Zbl 0699.68020  Leivant, D., Reasoning about functional programs and complexity classes associated with type disciplines, (24th Ann. Symp. on Foundations of Computer Science, vol. 44 (1983)), 460-469  Nour, K., Opérateurs de mise en mémoire en lambda-calcul pur et typé, (Ph.D. Thesis (1993), Université de Savoie)  Nour, K., A general type for storage operator, Math. Logic Quart., 41, 505-514 (1995) · Zbl 0837.03014  Nour, K., Storage operator and ∀-positive types in system TTR, Math. Logic Quart., 42, 2, 349-368 (1996) · Zbl 0852.03006  Nour, K., Storage operators and ∀-positive types, Inform. Théorique Appl., 30, 3, 261-293 (1996) · Zbl 0869.03009  Nour, K.; David, R., Storage operator and directed λ-calculus, J. Symbolic Logic, 60, 4, 1050-1086 (1995) · Zbl 0852.03007  Parigot, M., Recursive programming with proofs, Theoret. Comput. Sci., 94, 335-356 (1992) · Zbl 0759.68014  Parigot, M., Strong normalization for second order classical natural deduction, Logic Comput. Sci., 39-46 (1993)  Raffalli, C., L’ Arithmétiques Fonctionnelle du Second Ordre avec Points Fixes, (Ph.D. Thesis (Février 1994), Université Paris 7)
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.