Extending the Curry-Howard interpretation to linear, relevant and other resource logics

DOI10.2307/2275370zbMath0765.03005OpenAlexW2134870220WikidataQ56211001 ScholiaQ56211001MaRDI QIDQ4032664

Ruy J. G. B. de Queiroz, Dov M. Gabbay

Publication date: 1 April 1993

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2307/2275370

zbMATH Keywords

linear restrictionCurry- Howard interpretationrelevance restriction for implicationresource implications

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40)

Related Items

The placeholder view of assumptions and the Curry-Howard correspondence, Cut Elimination for Extended Sequent Calculi, A proof-theoretic investigation of a logic of positions, Covert Movement in Logical Grammar, The Functional Interpretation of Direct Computations, On reduction rules, meaning-as-use, and proof-theoretic semantics, Cut-free Gentzen calculus for multimodal CK, Natural Deduction for Equality: The Missing Entity

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Normalization and excluded middle. I
• Intuitionism. An introduction
• An axiomatization of the finite-valued Łukasiewicz calculus
• Sequent-systems and groupoid models. I
• Logic colloquium '73. Proceedings of the logic colloquium, Bristol, July 1973
• Sequent-systems and groupoid models. II
• The universal quantifier in combinatory logic
• Combinatory logic. Vol. II
• Proof theory and computer programming
• The Mathematics of Sentence Structure
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Abstract Data Types and Type Theory: Theories as Types
• Logics without the contraction rule
• A Proof-Theoretic Account of Programming and the Role of Reduction Rules
• Functionality in Combinatory Logic
• The combinatory foundations of mathematical logic