A general storage theorem for integers in call-by-name \(\lambda\)- calculus (Q1329740): Difference between revisions
From MaRDI portal
Set OpenAlex properties. |
ReferenceBot (talk | contribs) Changed an Item |
||
Property / cites work | |||
Property / cites work: Q5625124 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4274979 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Opérateurs de mise en mémoire et traduction de Gödel. (Storage operators and Gödel translation) / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Lambda-calcul, évaluation paresseuse et mise en mémoire / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Classical logic, storage operators and second-order lambda-calculus / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3477935 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4264064 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4255509 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Call-by-name, call-by-value and the \(\lambda\)-calculus / rank | |||
Normal rank |
Latest revision as of 17:07, 22 May 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
0 references