Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

Mixed logic and storage operators

Karim Nour1

(1)  LAMA – Equipe de Logique, Université de Chambéry, 73376 Le Bourget du Lac, France. e-mail: nour@univ-savoie.fr, FR
Abstract.   In 1990 J-L. Krivine introduced the notion of storage operators. They are -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 the classical logic. In his system the property of the unicity of integers 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.
Received: 7 May 1997

Fulltext Preview (Small, Large)
Image of the first page of the fulltext


Export this article
Export this article as RIS | Text
 
Remote Address: 38.107.191.100 • Server: mpweb17
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)