Mixed logic and storage operators (Q1570018)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Mixed logic and storage operators |
scientific article |
Statements
Mixed logic and storage operators (English)
0 references
9 July 2000
0 references
In 1990 J.-L. Krivine introduced the notion of storage operators. They are \(\lambda\)-terms which simulate call-by-value in the call-by-name strategy and they can be used in order to modelize assignment instructions. J.-L. Krivine has shown that there is a very simple second-order type in \(AF2\) type system for storage operators using Gödel translation of classical to intuitionistic logic. In order to modelize the control operators, J.-L. Krivine has extended the system \(AF2\) to classical logic. In his system the property of the unicity of integer representation is lost, but he has shown that storage operators typable in the system \(AF2\) can be used to find the values of classical integers. In this paper, we present a new classical type system based on a logical system called mixed logic. We prove that in this system we can characterize, by types, the storage operators and the control operators.
0 references
\(AF2\) type system
0 references
lambda calculus
0 references
storage operators
0 references
classical type system
0 references
mixed logic
0 references
control operators
0 references