Full intuitionistic linear logic

DOI10.1016/0168-0072(93)90146-5MaRDI QIDQ1314646zbMATH OpenOpenAlexWikidataFDO

Authors Martin Hyland, Valeria de Paiva

Publication date 27 March 1994

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0168-0072(93)90146-5

zbMATH Keywords

cut eliminationcategorical modelsmultiplicative disjunctionFull Intuitionistic Linear Logicinterpretation of proofsterm assignment system

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20) Metamathematics of constructive systems (03F50) Categorical logic, topoi (03G30)

Recommendations

• A Parigot-style linear \(\lambda\)-calculus for full intuitionistic linear logic
• scientific article; zbMATH DE number 2079022
• Multiple conclusion linear logic: cut elimination and more
• A note on full intuitionistic linear logic

Cites work

• scientific article; zbMATH DE number 431760 (Why is no real title available?)
• scientific article; zbMATH DE number 4055576 (Why is no real title available?)
• scientific article; zbMATH DE number 4103051 (Why is no real title available?)
• scientific article; zbMATH DE number 4104952 (Why is no real title available?)
• scientific article; zbMATH DE number 47172 (Why is no real title available?)
• scientific article; zbMATH DE number 176206 (Why is no real title available?)
• scientific article; zbMATH DE number 1324438 (Why is no real title available?)
• scientific article; zbMATH DE number 4122189 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3305156 (Why is no real title available?)
• *-autonomous categories. With an appendix by Po-Hsiang Chu
• A dialectica-like model of linear logic
• A game semantics for linear logic
• Normalization as a homomorphic image of cut-elimination
• Polycategories
• Proof theory
• Some Syntactical Observations on Linear Logic
• The correspondence between cut-elimination and normalization
• The system \({\mathcal F}\) of variable types, fifteen years later

Cited in

(31)

• Annotation-free sequent calculi for full intuitionistic linear logic
• New Curry-Howard terms for full linear logic
• Experiments in linear natural deduction
• Multiple conclusion linear logic: cut elimination and more
• Functional Interpretations of Intuitionistic Linear Logic
• Constructing Fully Complete Models of Multiplicative Linear Logic
• 1998 European Summer Meeting of the Association for Symbolic Logic
• Assertions, Hypotheses, Conjectures, Expectations: Rough-Sets Semantics and Proof Theory
• A formalization of Kant's transcendental logic
• Jets and differential linear logic
• Proof theory in the abstract
• Functional interpretations of intuitionistic linear logic
• Multiple conclusion linear logic: cut elimination and more
• A Parigot-style linear \(\lambda\)-calculus for full intuitionistic linear logic
• Investigations into a left-structural right-substructural sequent calculus
• scientific article; zbMATH DE number 4116494 (Why is no real title available?)
• Eilenberg-Kelly reloaded
• Coherence via focusing for symmetric skew monoidal categories
• PURE LOGIC OF ITERATED FULL GROUND
• scientific article; zbMATH DE number 218517 (Why is no real title available?)
• Commutative Lambek grammars
• A note on full intuitionistic linear logic
• Clones, closed categories, and combinatory logic
• On sheaf cohomology and natural expansions
• scientific article; zbMATH DE number 2079022 (Why is no real title available?)
• scientific article; zbMATH DE number 7359406 (Why is no real title available?)
• On the meaning of logical rules. II: Multiplicatives and additives
• Realizability Proof for Normalization of Full Differential Linear Logic
• A normalizing system of natural deduction for intuitionistic linear logic
• Monoidal logics: completeness and classical systems
• A comparison between monoidal and substructural logics

This page was built for publication: Full intuitionistic linear logic

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