A general storage theorem for integers in call-by-name \(\lambda\)- calculus
type: Item
instance of: scholarly article
title: A general storage theorem for integers in call-by-name \(\lambda\)- calculus
zbMATH Open document ID: 0813.03008
DOI: 10.1016/0304-3975(94)90081-7
author: Jean-Louis Krivine
published in: Theoretical Computer Science
publication date: 1995-05-18T00:00:00Z
review text: The result presented here is part of a general program which aims at proving that all features of imperative programming can be efficiently simulated within (lazy) call-by-name \(\lambda\)-calculus. The notion of ``storage operators'' has been introduced by the author in order to simulate the call-by-value strategy and to modelize assignment instructions. The main result about storage operators is that there is a simple second- order type for them, using Gödel's not-not-translation. Krivine gives here a new and simpler proof of a stronger version of this theorem, which contains in particular his previous results concerning the typing of storage operators in intuitionistic and in classical logic. This striking result, whose proof remains technically involved, gives rise to new storage theorems, and can be given a rather intuitive meaning in terms of realisability.
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 68N01
Mathematics Subject Classification ID: 03B15
zbMATH DE Number: 612371
zbMATH Keywords: Gödel's translation
zbMATH Keywords: imperative programming
zbMATH Keywords: call-by-name \(\lambda\)-calculus
zbMATH Keywords: storage operators
reviewed by: Chantal Berline
MaRDI profile type: Publication
full work available at URL: 0304-3975(94)90081-7
OpenAlex ID: W2085642842
cites work: Q5625124
cites work: Q4274979
cites work: Opérateurs de mise en mémoire et traduction de Gödel. (Storage operators and Gödel translation)
cites work: Lambda-calcul, évaluation paresseuse et mise en mémoire
cites work: Classical logic, storage operators and second-order lambda-calculus
cites work: Q3477935
cites work: Q4264064
cites work: Q4255509
cites work: Call-by-name, call-by-value and the \(\lambda\)-calculus
description: scientific article; zbMATH DE number 612371