Composition of deductions within the propositions-as-types paradigm

DOI10.1007/s11787-020-00260-3zbMath1485.03231OpenAlexW3082827625MaRDI QIDQ2228351

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

cut ruleCurry-Howard isomorphismgeneral proof theorycategorial proof theorycomposition of deductionconstructive-type theorypropositions as types

Mathematics Subject Classification ID

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

Uses Software

• Pesca

Cites Work

• The categorical and the hypothetical: a critique of some fundamental assumptions of standard semantics
• Combinatory logic. With two sections by William Craig.
• The calculus of constructions
• Immanent reasoning or equality in action. A plaidoyer for the play level
• Revisiting the categorical interpretation of dependent type theory
• Towards a more general concept of inference
• Locally cartesian closed categories and type theory
• Functional completeness of cartesian categories
• Inferential Semantics
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Deductive Completeness
• On the Paths of Categories
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item