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

DOI10.2307/2275370MaRDI QIDQ4032664zbMATH OpenOpenAlexWikidataFDO

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

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)

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

Cites work

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

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)