Composition of deductions within the propositions-as-types paradigm

DOI10.1007/S11787-020-00260-3MaRDI QIDQ2228351zbMATH OpenOpenAlexFDO

Authors Ivo Pezlar

Publication date 17 February 2021

Published in Logica Universalis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s11787-020-00260-3

zbMATH Keywords

categorial proof theorycomposition of deductionconstructive-type theoryCurry-Howard isomorphismcut rulegeneral proof theorypropositions as types

Mathematics Subject Classification ID

Higher-order logic (03B16) Combinatory logic and lambda calculus (03B40) Proof theory in general (including proof-theoretic semantics) (03F03)

Recommendations

• Deduction as reduction, from a categorical point of view
• The Significance of the Curry-Howard Isomorphism
• Proof theory in the abstract
• A prologue to the theory of deduction
• scientific article; zbMATH DE number 963644

Cites work

• Combinatory logic. With two sections by William Craig.
• Deductive Completeness
• Functional completeness of cartesian categories
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 1823815 (Why is no real title available?)
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 3521950 (Why is no real title available?)
• scientific article; zbMATH DE number 591911 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3360143 (Why is no real title available?)
• Immanent reasoning or equality in action. A plaidoyer for the play level
• Inferential Semantics
• Locally cartesian closed categories and type theory
• On the Paths of Categories
• Revisiting the categorical interpretation of dependent type theory
• Structural proof theory. With an appendix by Aarne Ranta
• The calculus of constructions
• The categorical and the hypothetical: a critique of some fundamental assumptions of standard semantics
• Towards a more general concept of inference

Cited in

(2)

• Composition under distributive natural transformations: or, when predicate abstraction is impossible
• Hyperintensions as computations

Describes a project that uses

Uses Software

• Pesca

This page was built for publication: Composition of deductions within the propositions-as-types paradigm

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