A General Type for Storage Operators

DOI10.1002/MALQ.19950410407MaRDI QIDQ4857862zbMATH OpenOpenAlexFDO

Authors Karim Nour

Publication date 13 May 1996

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

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

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)

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.

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

Cited in

(5)

• A semantical storage operator theorem for all types
• Mixed logic and storage operators
• scientific article; zbMATH DE number 458872 (Why is no real title available?)
• 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)