On Storage Operators

TL;DR

This paper reviews the concept of storage operators in lambda calculus, highlighting their role in simulating call-by-value, their typing in AF2, and their significance in classical logic, synthesizing key results in the field.

Contribution

It provides a comprehensive synthesis of existing results on storage operators, emphasizing their types, logical significance, and applications.

Findings

Storage operators simulate call-by-value in call-by-name.

A simple AF2 type for storage operators is identified.

Storage operators are crucial tools in classical logic.

Abstract

In 1990 Krivine introduced the notion of storage operators. They are $\lambda$-terms which simulate call-by-value in the call-by-name strategy. Krivine has shown that there is a very simple type in the AF2 type system for storage operators using G\"odel translation from classical to intuitionistic logic. Parigot and Krivine have shown that storage operators play an important tool in classical logic. In this paper, we present a synthesis of various results on this subject.