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

DOI10.2307/2275370zbMATH Open0765.03005OpenAlexW2134870220WikidataQ56211001 ScholiaQ56211001MaRDI QIDQ4032664FDOQ4032664

Authors: Ruy J. G. B. de Queiroz, Dov 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

Recommendations

• Curry-Howard terms for linear logic
• scientific article; zbMATH DE number 963644
• scientific article; zbMATH DE number 2079016
• scientific article; zbMATH DE number 786485
• Manipulating sources of information: towards an interpretation of linear logic and strong relevance logic

zbMATH Keywords

linear restrictionCurry- Howard interpretationrelevance restriction for implicationresource implications

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (9)

• New Curry-Howard terms for full linear logic
• The functional interpretation of direct computations
• Natural Deduction for Equality: The Missing Entity
• On reduction rules, meaning-as-use, and proof-theoretic semantics
• The placeholder view of assumptions and the Curry-Howard correspondence
• Cut-free Gentzen calculus for multimodal CK
• Cut Elimination for Extended Sequent Calculi
• A proof-theoretic investigation of a logic of positions
• Covert movement in logical grammar

This page was built for publication: Extending the Curry-Howard interpretation to linear, relevant and other resource logics

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