Closed categories and the theory of proofs

DOI10.1007/BF01404107zbMath0449.03054OpenAlexW1991895871MaRDI QIDQ1147133

Grigori Mints

Publication date: 1981

Published in: Journal of Soviet Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01404107

zbMATH Keywords

proof theorydecision procedurecoherence theorem for canonical morphismsequality of canonical morphismslambda languagetheory of proofsthinning rule

Mathematics Subject Classification ID

Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Foundations, relations to logic and deductive systems (18A15) Proof theory and constructive mathematics (03F99)

Related Items (14)

Coherence in SMCCs and equivalences on derivations in IMML with unit ⋮ Proof of a S.Mac Lane conjecture (extended abstract) ⋮ Proof of a conjecture of S. Mac Lane ⋮ Natural deduction and coherence for weakly distributive categories ⋮ Developing developments ⋮ On categorical equivalence of Gentzen-style derivations in IMLL ⋮ Three faces of natural deduction ⋮ Unnamed Item ⋮ Categorical interpretation of logical derivations and its applications in algebra ⋮ Game Semantics and Uniqueness of Type Inhabitance in the Simply-Typed λ-Calculus ⋮ Covert Movement in Logical Grammar ⋮ Linear logic, coherence and dinaturality ⋮ On the conditions of full coherence in closed categories ⋮ Multiplicative Linear Logics and Fibrations

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A categorical equivalence of proofs
• A generalization of the functorial calculus
• Coherence in closed categories
• The correspondence between cut-elimination and normalization
• The Connection between Equivalence of Proofs and Cartesian Closed Categories
• Topology and logic as a source of algebra
• Deductive systems and categories

This page was built for publication: Closed categories and the theory of proofs