A general storage theorem for integers in call-by-name \(\lambda\)- calculus (Q1329740): Difference between revisions
From MaRDI portal
Set profile property. |
Set OpenAlex properties. |
||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1016/0304-3975(94)90081-7 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2085642842 / rank | |||
Normal rank |
Revision as of 02:15, 20 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | A general storage theorem for integers in call-by-name \(\lambda\)- calculus |
scientific article |
Statements
A general storage theorem for integers in call-by-name \(\lambda\)- calculus (English)
0 references
18 May 1995
0 references
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.
0 references
Gödel's translation
0 references
imperative programming
0 references
call-by-name \(\lambda\)-calculus
0 references
storage operators
0 references