scientific article; zbMATH DE number 65742

MaRDI QIDQ4010353zbMATH OpenFDO

Authors Roberto Di Cosmo, Giuseppe Longo

Publication date 27 September 1992

zbMATH Keywords

cartesian closed categoryconstructive equivalenceIntuitionistic propositional calculus

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40) Proof theory in general (including proof-theoretic semantics) (03F03) Natural morphisms, dinatural morphisms (18A23) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15)

Recommendations

• scientific article; zbMATH DE number 65746
• scientific article; zbMATH DE number 3928997
• Provable isomorphisms of types
• Quantifier-complete categories
• Isomorphic formulae in classical propositional logic

Cited in

(7)

• Quantifier-complete categories
• The genericity theorem and parametricity in the polymorphic \(\lambda\)- calculus
• Isomorphic formulae in classical propositional logic
• scientific article; zbMATH DE number 65746 (Why is no real title available?)
• Provable isomorphisms of types
• scientific article; zbMATH DE number 1285752 (Why is no real title available?)
• Proof normalisation in a logic identifying isomorphic propositions

This page was built for publication:

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