A General Type for Storage Operators

DOI10.1002/MALQ.19950410407zbMATH Open0837.03014arXiv0905.0549OpenAlexW2963573047MaRDI QIDQ4857862FDOQ4857862

Authors: Karim Nour 

Publication date: 13 May 1996

Published in: Mathematical Logic Quarterly (Search for Journal in Brave)

Abstract: In 1990, J.L. Krivine introduced the notion of storage operator to simulate, in $lambda$-calculus, the "call by value" in a context of a "call by name". J.L. Krivine has shown that, using G"odel translation from classical into intuitionistic logic, we can find a simple type for storage operators in AF2 type system. In this present paper, we give a general type for storage operators in a slight extension of AF2. We give at the end (without proof) a generalization of this result to other types.

Full work available at URL: https://arxiv.org/abs/0905.0549

Recommendations

• Opérateurs de mise en mémoire et types $\forall $-positifs
• Mixed logic and storage operators
• scientific article; zbMATH DE number 458872
• scientific article; zbMATH DE number 563671
• A semantical storage operator theorem for all types

zbMATH Keywords

typed \(\lambda\)-calculusdata typehead normal formChurch integerhead reductionAF2 type systemstorage operatorGödel translation\(\beta\)-equivalence

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Combinatory logic and lambda calculus (03B40)

Cited In (5)

• A semantical storage operator theorem for all types
• Mixed logic and storage operators
• Title not available (Why is that?)
• A general storage theorem for integers in call-by-name \(\lambda\)- calculus
• Storage Operators and ∀‐positive Types in TTR Type System

This page was built for publication: A General Type for Storage Operators

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4857862)