Storage operators and forall-positive types of system TTR
From MaRDI portal
Publication:6213794
DOI10.1002/MALQ.19960420130arXiv0905.0550MaRDI QIDQ6213794
Publication date: 5 May 2009
Abstract: In 1990, J.L. Krivine introduced the notion of storage operator to simulate "call by value" in the "call by name" strategy. J.L. Krivine has shown that, using G"odel translation of classical into intuitionitic logic, we can find a simple type for the storage operators in AF2 type system. This paper studies the -positive types (the universal second order quantifier appears positively in these types), and the G"odel transformations (a generalization of classical G"odel translation) of TTR type system. We generalize, by using syntaxical methods, the J.L. Krivine's Theorem about these types and for these transformations. We give a proof of this result in the case of the type of recursive integers.
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Combinatory logic and lambda calculus (03B40)
This page was built for publication: Storage operators and forall-positive types of system TTR
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6213794)
